defpred S₁[ object , object ] means ex x being variable ex T being quasi-type st
( $1 = x & $2 = T & vars T = vars x );
A1: for z being object st z in rng l holds
ex y being object st S₁[z,y]

proof

set C = MaxConstrSign ;
let z be object ; :: thesis: ( z in rng l implies ex y being object st S₁[z,y] )
assume z in rng l ; :: thesis: ex y being object st S₁[z,y]
then reconsider x = z as variable ;
varcl (vars x) = vars x by Th2;
then consider m being constructor OperSymbol of a_Type MaxConstrSign, p being FinSequence of QuasiTerms MaxConstrSign such that
A2: ( len p = len (the_arity_of m) & vars (m -trm p) = vars x ) by Th59;
( a_Type MaxConstrSign in the carrier of MaxConstrSign & the carrier of MaxConstrSign c= rng the ResultSort of MaxConstrSign ) by ABCMIZ_1:def 54;
then consider o being object such that
A3: ( o in dom the ResultSort of MaxConstrSign & a_Type MaxConstrSign = the ResultSort of MaxConstrSign . o ) by FUNCT_1:def 3;
reconsider o = o as OperSymbol of MaxConstrSign by A3;
the_result_sort_of o = a_Type MaxConstrSign by A3;
then the_result_sort_of m = a_Type MaxConstrSign by ABCMIZ_1:def 32;
then reconsider q = m -trm p as pure expression of MaxConstrSign , a_Type MaxConstrSign by A2, ABCMIZ_1:75;
set B = {} (QuasiAdjs MaxConstrSign);
reconsider T = ({} (QuasiAdjs MaxConstrSign)) ast q as quasi-type ;
take T ; :: thesis: S₁[z,T]
take x ; :: thesis: ex T being quasi-type st
( z = x & T = T & vars T = vars x )
take T ; :: thesis: ( z = x & T = T & vars T = vars x )
thus ( z = x & T = T & vars T = vars x ) by A2, ABCMIZ_1:106; :: thesis: verum

end;

consider f being Function such that
A4: dom f = rng l and
A5: for z being object st z in rng l holds
S₁[z,f . z] from CLASSES1:sch 1(A1);
rng f c= QuasiTypes

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in QuasiTypes )
assume y in rng f ; :: thesis: y in QuasiTypes
then consider z being object such that
A6: ( z in dom f & y = f . z ) by FUNCT_1:def 3;
S₁[z,y] by A4, A5, A6;
hence y in QuasiTypes by ABCMIZ_1:def 43; :: thesis: verum

end;

then reconsider f = f as PartFunc of Vars,QuasiTypes by A4, RELSET_1:4;
take f ; :: thesis: ( dom f = rng l & f is even )
thus dom f = rng l by A4; :: thesis: f is even
let x be variable; :: according to ABCMIZ_A:def 29 :: thesis: for T being quasi-type st x in dom f & T = f . x holds
vars T = vars x
let T be quasi-type; :: thesis: ( x in dom f & T = f . x implies vars T = vars x )
assume ( x in dom f & T = f . x ) ; :: thesis: vars T = vars x
then S₁[x,T] by A4, A5;
hence vars T = vars x ; :: thesis: verum