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
A5: len a1 = len l and
A6: for i being Nat st i in dom l holds
a1 . i = (l /. i) -term MaxConstrSign and
A7: len a2 = len l and
A8: for i being Nat st i in dom l holds
a2 . i = (l /. i) -term MaxConstrSign ; :: thesis: a1 = a2
A9: ( dom a1 = dom l & dom a2 = dom l ) by A5, A7, FINSEQ_3:29;

now :: thesis: for i being Nat st i in dom a1 holds
a1 . i = a2 . i

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 A6, A8, A9;
hence a1 . i = a2 . i ; :: thesis: verum

end;

hence a1 = a2 by A9; :: thesis: verum