let i be Nat; :: thesis: for R, R1 being i -element FinSequence of COMPLEX holds R1 = (R1 + R) - R
let R, R1 be i -element FinSequence of COMPLEX ; :: thesis: R1 = (R1 + R) - R
thus R1 = R1 + (i |-> 0c) by BINOP_2:1, FINSEQOP:56
.= R1 + (R - R) by BINOP_2:1, FINSEQOP:73, SEQ_4:51, SEQ_4:52
.= (R1 + R) - R by RFUNCT_1:23 ; :: thesis: verum