let k, n be Nat; :: thesis: for c1, c2 being Element of COMPLEX
for z1, z2 being Element of COMPLEX n st k in Seg n & c1 = z1 . k & c2 = z2 . k holds
(z1 + z2) . k = c1 + c2
let c1, c2 be Element of COMPLEX ; :: thesis: for z1, z2 being Element of COMPLEX n st k in Seg n & c1 = z1 . k & c2 = z2 . k holds
(z1 + z2) . k = c1 + c2
let z1, z2 be Element of COMPLEX n; :: thesis: ( k in Seg n & c1 = z1 . k & c2 = z2 . k implies (z1 + z2) . k = c1 + c2 )
assume that
A1: k in Seg n and
A2: ( c1 = z1 . k & c2 = z2 . k ) ; :: thesis: (z1 + z2) . k = c1 + c2
k in dom (z1 + z2) by A1, Lm4;
hence (z1 + z2) . k = addcomplex . (c1,c2) by A2, FUNCOP_1:22
.= c1 + c2 by BINOP_2:def 3 ;
:: thesis: verum