let l1, l2 be FinSequence of QC-variables ; :: thesis: ( len l1 = len l & ( for k being Element of 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 Element of 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 Element of 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 Element of 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

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: k in NAT by ORDINAL1:def 13;
then A13: ( 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, A12, A11;
hence l1 . k = l2 . k by A10, A12, A11, A13; :: thesis: verum

end;

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