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

proof

let j be set ; :: 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 set such that
A3: ( z in dom g & j = g . z ) by FUNCT_1:def 5;
reconsider z = z as Nat by A3;
j = H₁(z) by A1, A3;
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 A0, A1, A2; :: thesis: verum