let k, n be Nat; :: thesis: for z1, z2 being Element of COMPLEX n st k in Seg n holds
(z1 - z2) . k = (z1 . k) - (z2 . k)
let z1, z2 be Element of COMPLEX n; :: thesis: ( k in Seg n implies (z1 - z2) . k = (z1 . k) - (z2 . k) )
assume A1: k in Seg n ; :: thesis: (z1 - z2) . k = (z1 . k) - (z2 . k)
set c1 = z1 . k;
set c2 = z2 . k;
k in dom (z1 - z2) by A1, Lm4;
hence (z1 - z2) . k = diffcomplex . ((z1 . k),(z2 . k)) by FUNCOP_1:22
.= (z1 . k) - (z2 . k) by BINOP_2:def 4 ;
:: thesis: verum