let a1, a2 be Real_Sequence; :: thesis: ( ( for i being Nat holds a1 . i = ((- 1) |^ i) * (a . i) ) & ( for i being Nat holds a2 . i = ((- 1) |^ i) * (a . i) ) implies a1 = a2 )
assume that
A3: for i being Nat holds a1 . i = ((- 1) |^ i) * (a . i) and
A4: for i being Nat holds a2 . i = ((- 1) |^ i) * (a . i) ; :: thesis: a1 = a2
now :: thesis: for x being object st x in NAT holds
a1 . x = a2 . x
let x be object ; :: thesis: ( x in NAT implies a1 . x = a2 . x )
assume x in NAT ; :: thesis: a1 . x = a2 . x
then reconsider i = x as Nat ;
thus a1 . x = ((- 1) |^ i) * (a . i) by A3
.= a2 . x by A4 ; :: thesis: verum
end;
hence a1 = a2 ; :: thesis: verum