let i be Nat; :: thesis: for c1, c2 being Complex holds (i |-> c1) - (i |-> c2) = i |-> (c1 - c2)

let c1, c2 be Complex; :: thesis: (i |-> c1) - (i |-> c2) = i |-> (c1 - c2)

reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;

(i |-> s1) - (i |-> s2) = i |-> (diffcomplex . (s1,s2)) by FINSEQOP:17

.= i |-> (c1 - c2) by BINOP_2:def 4 ;

hence (i |-> c1) - (i |-> c2) = i |-> (c1 - c2) ; :: thesis: verum

let c1, c2 be Complex; :: thesis: (i |-> c1) - (i |-> c2) = i |-> (c1 - c2)

reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;

(i |-> s1) - (i |-> s2) = i |-> (diffcomplex . (s1,s2)) by FINSEQOP:17

.= i |-> (c1 - c2) by BINOP_2:def 4 ;

hence (i |-> c1) - (i |-> c2) = i |-> (c1 - c2) ; :: thesis: verum