let seq, seq1, seq2 be complex-valued ManySortedSet of NAT ; :: thesis: ( seq = seq1 + seq2 iff for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) )

thus ( seq = seq1 + seq2 implies for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) :: thesis: ( ( for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) implies seq = seq1 + seq2 )

then A3: for n being object st n in dom seq holds

seq . n = (seq1 . n) + (seq2 . n) ;

dom seq = NAT /\ NAT by PARTFUN1:def 2

.= NAT /\ (dom seq2) by PARTFUN1:def 2

.= (dom seq1) /\ (dom seq2) by PARTFUN1:def 2 ;

hence seq = seq1 + seq2 by A3, VALUED_1:def 1; :: thesis: verum

thus ( seq = seq1 + seq2 implies for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) :: thesis: ( ( for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) implies seq = seq1 + seq2 )

proof

assume
for n being Nat holds seq . n = (seq1 . n) + (seq2 . n)
; :: thesis: seq = seq1 + seq2
assume A1:
seq = seq1 + seq2
; :: thesis: for n being Nat holds seq . n = (seq1 . n) + (seq2 . n)

let n be Nat; :: thesis: seq . n = (seq1 . n) + (seq2 . n)

A2: n in NAT by ORDINAL1:def 12;

dom seq = NAT by PARTFUN1:def 2;

hence seq . n = (seq1 . n) + (seq2 . n) by A1, VALUED_1:def 1, A2; :: thesis: verum

end;let n be Nat; :: thesis: seq . n = (seq1 . n) + (seq2 . n)

A2: n in NAT by ORDINAL1:def 12;

dom seq = NAT by PARTFUN1:def 2;

hence seq . n = (seq1 . n) + (seq2 . n) by A1, VALUED_1:def 1, A2; :: thesis: verum

then A3: for n being object st n in dom seq holds

seq . n = (seq1 . n) + (seq2 . n) ;

dom seq = NAT /\ NAT by PARTFUN1:def 2

.= NAT /\ (dom seq2) by PARTFUN1:def 2

.= (dom seq1) /\ (dom seq2) by PARTFUN1:def 2 ;

hence seq = seq1 + seq2 by A3, VALUED_1:def 1; :: thesis: verum