reconsider F3 = F1, F4 = F2 as FinSequence of COMPLEX by Lm2;

let F be FinSequence of COMPLEX ; :: thesis: ( F = F1 - F2 iff F = diffcomplex .: (F1,F2) )

A1: dom (F1 - F2) = (dom F1) /\ (dom F2) by VALUED_1:12;

dom diffcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1;

then A2: [:(rng F3),(rng F4):] c= dom diffcomplex by ZFMISC_1:96;

then A3: dom (diffcomplex .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69;

thus ( F = F1 - F2 implies F = diffcomplex .: (F1,F2) ) :: thesis: ( F = diffcomplex .: (F1,F2) implies F = F1 - F2 )

let F be FinSequence of COMPLEX ; :: thesis: ( F = F1 - F2 iff F = diffcomplex .: (F1,F2) )

A1: dom (F1 - F2) = (dom F1) /\ (dom F2) by VALUED_1:12;

dom diffcomplex = [:COMPLEX,COMPLEX:] by FUNCT_2:def 1;

then A2: [:(rng F3),(rng F4):] c= dom diffcomplex by ZFMISC_1:96;

then A3: dom (diffcomplex .: (F1,F2)) = (dom F1) /\ (dom F2) by FUNCOP_1:69;

thus ( F = F1 - F2 implies F = diffcomplex .: (F1,F2) ) :: thesis: ( F = diffcomplex .: (F1,F2) implies F = F1 - F2 )

proof

assume A5:
F = diffcomplex .: (F1,F2)
; :: thesis: F = F1 - F2
assume A4:
F = F1 - F2
; :: thesis: F = diffcomplex .: (F1,F2)

for z being set st z in dom (diffcomplex .: (F1,F2)) holds

F . z = diffcomplex . ((F1 . z),(F2 . z))

end;for z being set st z in dom (diffcomplex .: (F1,F2)) holds

F . z = diffcomplex . ((F1 . z),(F2 . z))

proof

hence
F = diffcomplex .: (F1,F2)
by A1, A3, A4, FUNCOP_1:21; :: thesis: verum
let z be set ; :: thesis: ( z in dom (diffcomplex .: (F1,F2)) implies F . z = diffcomplex . ((F1 . z),(F2 . z)) )

assume z in dom (diffcomplex .: (F1,F2)) ; :: thesis: F . z = diffcomplex . ((F1 . z),(F2 . z))

hence F . z = (F1 . z) - (F2 . z) by A1, A3, A4, VALUED_1:13

.= diffcomplex . ((F1 . z),(F2 . z)) by BINOP_2:def 4 ;

:: thesis: verum

end;assume z in dom (diffcomplex .: (F1,F2)) ; :: thesis: F . z = diffcomplex . ((F1 . z),(F2 . z))

hence F . z = (F1 . z) - (F2 . z) by A1, A3, A4, VALUED_1:13

.= diffcomplex . ((F1 . z),(F2 . z)) by BINOP_2:def 4 ;

:: thesis: verum

now :: thesis: for c being object st c in dom F holds

F . c = (F1 . c) - (F2 . c)

hence
F = F1 - F2
by A1, A2, A5, FUNCOP_1:69, VALUED_1:14; :: thesis: verumF . c = (F1 . c) - (F2 . c)

let c be object ; :: thesis: ( c in dom F implies F . c = (F1 . c) - (F2 . c) )

assume c in dom F ; :: thesis: F . c = (F1 . c) - (F2 . c)

hence F . c = diffcomplex . ((F1 . c),(F2 . c)) by A5, FUNCOP_1:22

.= (F1 . c) - (F2 . c) by BINOP_2:def 4 ;

:: thesis: verum

end;assume c in dom F ; :: thesis: F . c = (F1 . c) - (F2 . c)

hence F . c = diffcomplex . ((F1 . c),(F2 . c)) by A5, FUNCOP_1:22

.= (F1 . c) - (F2 . c) by BINOP_2:def 4 ;

:: thesis: verum