let a1, a2 be FinSequence of QuasiTerms MaxConstrSign; :: thesis: ( len a1 = len l & ( for i being Nat st i in dom l holds
a1 . i = (l /. i) -term MaxConstrSign ) & len a2 = len l & ( for i being Nat st i in dom l holds
a2 . i = (l /. i) -term MaxConstrSign ) implies a1 = a2 )
assume that
A1: len a1 = len l and
A2: for i being Nat st i in dom l holds
a1 . i = (l /. i) -term MaxConstrSign and
A3: len a2 = len l and
A4: for i being Nat st i in dom l holds
a2 . i = (l /. i) -term MaxConstrSign ; :: thesis: a1 = a2
A5: ( dom a1 = dom l & dom a2 = dom l ) by A1, A3, FINSEQ_3:31;

now

let i be Nat; :: thesis: ( i in dom a1 implies a1 . i = a2 . i )
assume i in dom a1 ; :: thesis: a1 . i = a2 . i
then ( a1 . i = (l /. i) -term MaxConstrSign & a2 . i = (l /. i) -term MaxConstrSign ) by A2, A4, A5;
hence a1 . i = a2 . i ; :: thesis: verum

end;

hence a1 = a2 by A5, FINSEQ_1:17; :: thesis: verum