let C be initialized ConstructorSignature; :: thesis: for f being one-to-one irrelevant valuation of C ex g being one-to-one irrelevant valuation of C st
for x, y being variable holds
( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )
let f be one-to-one irrelevant valuation of C; :: thesis: ex g being one-to-one irrelevant valuation of C st
for x, y being variable holds
( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )
set Y = { x where x is variable : x -term C in rng f } ;
defpred S₁[ set , set ] means ex x being set st
( x in dom f & f . x = root-tree [$1,a_Term ] & $2 = root-tree [x,a_Term ] );
B1: for x being set st x in { x where x is variable : x -term C in rng f } holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in { x where x is variable : x -term C in rng f } implies ex y being set st S₁[x,y] )
assume x in { x where x is variable : x -term C in rng f } ; :: thesis: ex y being set st S₁[x,y]
then B2: ex z being variable st
( x = z & z -term C in rng f ) ;
then reconsider z = x as variable ;
consider y being set such that
B3: ( y in dom f & z -term C = f . y ) by B2, FUNCT_1:def 5;
reconsider y = y as variable by B3;
take y -term C ; :: thesis: S₁[x,y -term C]
thus S₁[x,y -term C] by B3; :: thesis: verum

end;

consider g being Function such that
A0: dom g = { x where x is variable : x -term C in rng f } and
A1: for y being set st y in { x where x is variable : x -term C in rng f } holds
S₁[y,g . y] from CLASSES1:sch 1(B1);
A2: { x where x is variable : x -term C in rng f } c= Vars

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is variable : x -term C in rng f } or x in Vars )
assume x in { x where x is variable : x -term C in rng f } ; :: thesis: x in Vars
then ex z being variable st
( x = z & z -term C in rng f ) ;
hence x in Vars ; :: thesis: verum

end;

rng g c= QuasiTerms C

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in QuasiTerms C )
assume y in rng g ; :: thesis: y in QuasiTerms C
then consider x being set such that
C2: ( x in dom g & y = g . x ) by FUNCT_1:def 5;
reconsider x = x as variable by A0, A2, C2;
consider z being set such that
C3: ( z in dom f & f . z = x -term C & g . x = root-tree [z,a_Term ] ) by A0, A1, C2;
reconsider z = z as variable by C3;
y = z -term C by C2, C3;
hence y in QuasiTerms C by ELEMENT; :: thesis: verum

end;

then reconsider g = g as valuation of C by A0, A2, RELSET_1:11;
A3: g is irrelevant

proof

let x be variable; :: according to ABCMIZ_1:def 58 :: thesis: ( x in dom g implies ex y being variable st g . x = y -term C )
assume x in dom g ; :: thesis: ex y being variable st g . x = y -term C
then consider y being set such that
C1: ( y in dom f & f . y = x -term C & g . x = root-tree [y,a_Term ] ) by A0, A1;
reconsider y = y as variable by C1;
take y ; :: thesis: g . x = y -term C
thus g . x = y -term C by C1; :: thesis: verum

end;

g is one-to-one

proof

let z1, z2 be set ; :: according to FUNCT_1:def 8 :: thesis: ( not z1 in dom g or not z2 in dom g or not g . z1 = g . z2 or z1 = z2 )
assume C4: ( z1 in dom g & z2 in dom g & g . z1 = g . z2 ) ; :: thesis: z1 = z2
then reconsider z1 = z1, z2 = z2 as variable ;
consider x1 being set such that
C5: ( x1 in dom f & f . x1 = z1 -term C & g . z1 = root-tree [x1,a_Term ] ) by A0, A1, C4;
consider x2 being set such that
C6: ( x2 in dom f & f . x2 = z2 -term C & g . z1 = root-tree [x2,a_Term ] ) by A0, A1, C4;
reconsider x1 = x1, x2 = x2 as variable by C5, C6;
x1 -term C = x2 -term C by C5, C6;
then x1 = x2 by ThT0;
hence z1 = z2 by C5, C6, ThT0; :: thesis: verum

end;

then reconsider g = g as one-to-one irrelevant valuation of C by A3;
take g ; :: thesis: for x, y being variable holds
( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )
let x, y be variable; :: thesis: ( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )

hereby :: thesis: ( y in dom g & g . y = x -term C implies ( x in dom f & f . x = y -term C ) )

assume Z0: ( x in dom f & f . x = y -term C ) ; :: thesis: ( y in dom g & g . y = x -term C )
then f . x in rng f by FUNCT_1:def 5;
hence y in dom g by A0, Z0; :: thesis: g . y = x -term C
then S₁[y,g . y] by A0, A1;
hence g . y = x -term C by Z0, FUNCT_1:def 8; :: thesis: verum

end;

assume ( y in dom g & g . y = x -term C ) ; :: thesis: ( x in dom f & f . x = y -term C )
then consider z being set such that
Z2: ( z in dom f & f . z = root-tree [y,a_Term ] & x -term C = root-tree [z,a_Term ] ) by A0, A1;
reconsider z = z as variable by Z2;
x -term C = z -term C by Z2;
hence ( x in dom f & f . x = y -term C ) by Z2, ThT0; :: thesis: verum