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 Sub implies l1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l1 . k = l . k ) ) ) & len l2 = len l & ( for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies l2 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l2 . k = l . k ) ) ) implies l1 = l2 )
assume that
A9: len l1 = len l and
A10: for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies l1 . k = Sub . (l . k) ) & ( not l . k in dom Sub implies l1 . k = l . k ) ) and
A11: len l2 = len l and
A12: for k being Nat st 1 <= k & k <= len l holds
( ( l . k in dom Sub implies l2 . k = Sub . (l . k) ) & ( not l . k in dom Sub 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 A13: ( 1 <= k & k <= len l ) ; :: thesis: l1 . k = l2 . k
A14: ( not l . k in dom Sub implies l1 . k = l . k ) by A10, A13;
( l . k in dom Sub implies l1 . k = Sub . (l . k) ) by A10, A13;
hence l1 . k = l2 . k by A12, A13, A14; :: thesis: verum

end;

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