deffunc H₁( Nat) -> expression of MaxConstrSign , a_Term MaxConstrSign = (l /. $1) -term MaxConstrSign;
consider g being FinSequence such that
A1: len g = len l and
A2: for i being Nat st i in dom g holds
g . i = H₁(i) from FINSEQ_1:sch 2();
A3: dom g = dom l by A1, FINSEQ_3:29;
rng g c= QuasiTerms MaxConstrSign

proof

let j be object ; :: according to TARSKI:def 3 :: thesis: ( not j in rng g or j in QuasiTerms MaxConstrSign )
assume j in rng g ; :: thesis: j in QuasiTerms MaxConstrSign
then consider z being object such that
A4: ( z in dom g & j = g . z ) by FUNCT_1:def 3;
reconsider z = z as Nat by A4;
j = H₁(z) by A2, A4;
hence j in QuasiTerms MaxConstrSign by ABCMIZ_1:49; :: thesis: verum

end;

then reconsider g = g as FinSequence of QuasiTerms MaxConstrSign by FINSEQ_1:def 4;
take g ; :: thesis: ( len g = len l & ( for i being Nat st i in dom l holds
g . i = (l /. i) -term MaxConstrSign ) )
thus ( len g = len l & ( for i being Nat st i in dom l holds
g . i = (l /. i) -term MaxConstrSign ) ) by A1, A2, A3; :: thesis: verum