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₁[ object , object ] means ex x being set st
( x in dom f & f . x = root-tree [$1,a_Term] & $2 = root-tree [x,a_Term] );
A1: for x being object st x in { x where x is variable : x -term C in rng f } holds
ex y being object st S₁[x,y]

proof

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

end;

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

proof

let x be object ; :: 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 object ; :: 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 object such that
A8: x in dom g and
A9: y = g . x by FUNCT_1:def 3;
reconsider x = x as variable by A5, A7, A8;
consider z being set such that
A10: z in dom f and
f . z = x -term C and
A11: g . x = root-tree [z,a_Term] by A5, A6, A8;
reconsider z = z as variable by A10;
y = z -term C by A9, A11;
hence y in QuasiTerms C by Def28; :: thesis: verum

end;

then reconsider g = g as valuation of C by A5, A7, RELSET_1:4;
A12: 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
A13: y in dom f and
f . y = x -term C and
A14: g . x = root-tree [y,a_Term] by A5, A6;
reconsider y = y as variable by A13;
take y ; :: thesis: g . x = y -term C
thus g . x = y -term C by A14; :: thesis: verum

end;

g is one-to-one

proof

let z1, z2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not z1 in proj1 g or not z2 in proj1 g or not g . z1 = g . z2 or z1 = z2 )
assume that
A15: z1 in dom g and
A16: z2 in dom g and
A17: g . z1 = g . z2 ; :: thesis: z1 = z2
reconsider z1 = z1, z2 = z2 as variable by A15, A16;
consider x1 being set such that
A18: x1 in dom f and
A19: f . x1 = z1 -term C and
A20: g . z1 = root-tree [x1,a_Term] by A5, A6, A15;
consider x2 being set such that
A21: x2 in dom f and
A22: f . x2 = z2 -term C and
A23: g . z1 = root-tree [x2,a_Term] by A5, A6, A16, A17;
reconsider x1 = x1, x2 = x2 as variable by A18, A21;
x1 -term C = x2 -term C by A20, A23;
then x1 = x2 by Th50;
hence z1 = z2 by A19, A22, Th50; :: thesis: verum

end;

then reconsider g = g as one-to-one irrelevant valuation of C by A12;
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 that
A24: x in dom f and
A25: f . x = y -term C ; :: thesis: ( y in dom g & g . y = x -term C )
f . x in rng f by A24, FUNCT_1:def 3;
hence y in dom g by A5, A25; :: thesis: g . y = x -term C
then S₁[y,g . y] by A5, A6;
hence g . y = x -term C by A24, A25, FUNCT_1:def 4; :: thesis: verum

end;

assume that
A26: y in dom g and
A27: g . y = x -term C ; :: thesis: ( x in dom f & f . x = y -term C )
consider z being set such that
A28: z in dom f and
A29: f . z = root-tree [y,a_Term] and
A30: x -term C = root-tree [z,a_Term] by A5, A6, A26, A27;
reconsider z = z as variable by A28;
x -term C = z -term C by A30;
hence ( x in dom f & f . x = y -term C ) by A28, A29, Th50; :: thesis: verum