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 indom Sub implies l1 . k = Sub .(l . k) ) & ( not l . k indom Sub implies l1 . k = l . k ) ) ) & len l2 =len l & ( for k being Nat st 1 <= k & k <=len l holds ( ( l . k indom Sub implies l2 . k = Sub .(l . k) ) & ( not l . k indom 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 indom Sub implies l1 . k = Sub .(l . k) ) & ( not l . k indom 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 indom Sub implies l2 . k = Sub .(l . k) ) & ( not l . k indom Sub implies l2 . k = l . k ) )
; :: thesis: l1 = l2