let F1 be FinSequence of COMPLEX ; :: thesis: ( F1 = - F iff F1 = compcomplex * F )

A1: dom (- F) = dom F by VALUED_1:8;

A2: ( rng F c= COMPLEX & dom compcomplex = COMPLEX ) by FUNCT_2:def 1;

then A3: dom (compcomplex * F) = dom F by RELAT_1:27;

thus ( F1 = - F implies F1 = compcomplex * F ) :: thesis: ( F1 = compcomplex * F implies F1 = - F )

A1: dom (- F) = dom F by VALUED_1:8;

A2: ( rng F c= COMPLEX & dom compcomplex = COMPLEX ) by FUNCT_2:def 1;

then A3: dom (compcomplex * F) = dom F by RELAT_1:27;

thus ( F1 = - F implies F1 = compcomplex * F ) :: thesis: ( F1 = compcomplex * F implies F1 = - F )

proof

assume A6:
F1 = compcomplex * F
; :: thesis: F1 = - F
assume A4:
F1 = - F
; :: thesis: F1 = compcomplex * F

end;now :: thesis: for c being object st c in dom F1 holds

F1 . c = (compcomplex * F) . c

hence
F1 = compcomplex * F
by A3, A4, FUNCT_1:2, VALUED_1:8; :: thesis: verumF1 . c = (compcomplex * F) . c

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

assume A5: c in dom F1 ; :: thesis: F1 . c = (compcomplex * F) . c

thus F1 . c = - (F . c) by A4, VALUED_1:8

.= compcomplex . (F . c) by BINOP_2:def 1

.= (compcomplex * F) . c by A1, A4, A5, FUNCT_1:13 ; :: thesis: verum

end;assume A5: c in dom F1 ; :: thesis: F1 . c = (compcomplex * F) . c

thus F1 . c = - (F . c) by A4, VALUED_1:8

.= compcomplex . (F . c) by BINOP_2:def 1

.= (compcomplex * F) . c by A1, A4, A5, FUNCT_1:13 ; :: thesis: verum

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

(- F) . c = (compcomplex * F) . c

hence
F1 = - F
by A1, A2, A6, FUNCT_1:2, RELAT_1:27; :: thesis: verum(- F) . c = (compcomplex * F) . c

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

assume A7: c in dom F1 ; :: thesis: (- F) . c = (compcomplex * F) . c

thus (- F) . c = - (F . c) by VALUED_1:8

.= compcomplex . (F . c) by BINOP_2:def 1

.= (compcomplex * F) . c by A6, A7, FUNCT_1:12 ; :: thesis: verum

end;assume A7: c in dom F1 ; :: thesis: (- F) . c = (compcomplex * F) . c

thus (- F) . c = - (F . c) by VALUED_1:8

.= compcomplex . (F . c) by BINOP_2:def 1

.= (compcomplex * F) . c by A6, A7, FUNCT_1:12 ; :: thesis: verum