let seq1, seq2, seq3 be Complex_Sequence; :: thesis: ( seq1 = seq2 - seq3 iff for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) )

A1: ( ( for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 )

A1: ( ( for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 )

proof

( seq1 = seq2 - seq3 implies for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) )
assume A2:
for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)
; :: thesis: seq1 = seq2 - seq3

for x being object st x in NAT holds

seq1 . x = (seq2 - seq3) . x

end;for x being object st x in NAT holds

seq1 . x = (seq2 - seq3) . x

proof

hence
seq1 = seq2 - seq3
by FUNCT_2:12; :: thesis: verum
let x be object ; :: thesis: ( x in NAT implies seq1 . x = (seq2 - seq3) . x )

assume x in NAT ; :: thesis: seq1 . x = (seq2 - seq3) . x

then reconsider x = x as Element of NAT ;

seq1 . x = (seq2 . x) - (seq3 . x) by A2

.= (seq2 . x) + (- (seq3 . x))

.= (seq2 . x) + ((- seq3) . x) by VALUED_1:8

.= (seq2 + (- seq3)) . x by VALUED_1:1 ;

hence seq1 . x = (seq2 - seq3) . x ; :: thesis: verum

end;assume x in NAT ; :: thesis: seq1 . x = (seq2 - seq3) . x

then reconsider x = x as Element of NAT ;

seq1 . x = (seq2 . x) - (seq3 . x) by A2

.= (seq2 . x) + (- (seq3 . x))

.= (seq2 . x) + ((- seq3) . x) by VALUED_1:8

.= (seq2 + (- seq3)) . x by VALUED_1:1 ;

hence seq1 . x = (seq2 - seq3) . x ; :: thesis: verum

proof

hence
( seq1 = seq2 - seq3 iff for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n) )
by A1; :: thesis: verum
assume A3:
seq1 = seq2 - seq3
; :: thesis: for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)

end;now :: thesis: for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)

hence
for n being Nat holds seq1 . n = (seq2 . n) - (seq3 . n)
; :: thesis: verumlet n be Nat; :: thesis: seq1 . n = (seq2 . n) - (seq3 . n)

A4: n in NAT by ORDINAL1:def 12;

seq1 . n = (seq2 . n) + ((- seq3) . n) by A3, VALUED_1:1, A4

.= (seq2 . n) + (- (seq3 . n)) by VALUED_1:8 ;

hence seq1 . n = (seq2 . n) - (seq3 . n) ; :: thesis: verum

end;A4: n in NAT by ORDINAL1:def 12;

seq1 . n = (seq2 . n) + ((- seq3) . n) by A3, VALUED_1:1, A4

.= (seq2 . n) + (- (seq3 . n)) by VALUED_1:8 ;

hence seq1 . n = (seq2 . n) - (seq3 . n) ; :: thesis: verum