let C be initialized ConstructorSignature; :: thesis:
let f be one-to-one irrelevant valuation of C; :: thesis:
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]

let x be object ; :: thesis:
assume x in { x where x is variable : x -term C in rng f } ; :: thesis:
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:
thus S₁[x,y -term C] by A3, A4; :: thesis:

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

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

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng g ; :: thesis:
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:

end;

then reconsider g = g as valuation of C by A5, A7, RELSET_1:4;
A12: g is irrelevant

let x be variable; :: according to ABCMIZ_1:def 58 :: thesis:
assume x in dom g ; :: thesis:
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:
thus g . x = y -term C by A14; :: thesis:

end;

let z1, z2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A15: z1 in dom g and
A16: z2 in dom g and
A17: g . z1 = g . z2 ; :: thesis:
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:

end;

then reconsider g = g as one-to-one irrelevant valuation of C by A12;
take g ; :: thesis:
let x, y be variable; :: thesis:

end;

assume that
A26: y in dom g and
A27: g . y = x -term C ; :: thesis:
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: