let i be Nat; :: thesis: for R1, R being i -long FinSequence of COMPLEX holds R1 = (R1 - R) + R
let R1, R be i -long FinSequence of COMPLEX ; :: thesis: R1 = (R1 - R) + R
thus R1 = R1 + (i |-> 0c) by BINOP_2:1, FINSEQOP:57
.= R1 + ((- R) + R) by SEQ_4:68, SEQ_4:69, BINOP_2:1, FINSEQOP:77
.= (R1 - R) + R by FINSEQOP:29 ; :: thesis: verum