ficystodraunju lujvo

x1 is an injective function (distinctness-preserving function) from x2 (domain) to x3 (codomain).

This is a brapagjvo (one of its veljvo is the zi'evla "stodraunju"). Let f be the sumti which fills x1; for any y and z in x2, y =/= z iff f(y) =/= f(z).

In notes:

stodraunju
x1 is a function mapping x2 (domain) to x3 (codomain) such that properties x4 (ka) of x2 are preserved in its image under x1 according to the rules/operations/relations of x3 corresponding to those of x2 by x1.