let l1, l2 be FinSequence of QC-variables A; :: thesis: ( len l1 = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies l1 . k = f . (l . k) ) & ( not l . k in dom f implies l1 . k = l . k ) ) ) & len l2 = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies l2 . k = f . (l . k) ) & ( not l . k in dom f implies l2 . k = l . k ) ) ) implies l1 = l2 )
assume that
A7: len l1 = len l and
A8: for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies l1 . k = f . (l . k) ) & ( not l . k in dom f implies l1 . k = l . k ) ) and
A9: len l2 = len l and
A10: for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom f implies l2 . k = f . (l . k) ) & ( not l . k in dom f implies l2 . k = l . k ) ) ; :: thesis: l1 = l2

now :: thesis: for k being Nat st 1 <= k & k <= len l holds
l1 . k = l2 . k

let k be Nat; :: thesis: ( 1 <= k & k <= len l implies l1 . k = l2 . k )
assume A11: ( 1 <= k & k <= len l ) ; :: thesis: l1 . k = l2 . k
A12: ( not l . k in dom f implies l1 . k = l . k ) by A8, A11;
( l . k in dom f implies l1 . k = f . (l . k) ) by A8, A11;
hence l1 . k = l2 . k by A10, A11, A12; :: thesis: verum

end;

hence l1 = l2 by A7, A9, FINSEQ_1:14; :: thesis: verum