let x be Element of F_Complex; :: thesis: for z, w being Element of FQ x holds (FQ_add x) . (z,w) = z + w
let z, w be Element of FQ x; :: thesis: (FQ_add x) . (z,w) = z + w
thus (FQ_add x) . (z,w) = addcomplex . (z,w) by FUNCT_1:49, ZFMISC_1:87
.= z + w by BINOP_2:def 3 ; :: thesis: verum