let F1 be FinSequence of REAL ; :: thesis: ( F1 = - F iff F1 = compreal * F )
A1: dom (- F) = dom F by VALUED_1:8;
A2: ( rng F c= REAL & dom compreal = REAL ) by FUNCT_2:def 1;
then A3: dom (compreal * F) = dom F by RELAT_1:27;
thus ( F1 = - F implies F1 = compreal * F ) :: thesis: ( F1 = compreal * F implies F1 = - F )
proof
assume A4: F1 = - F ; :: thesis: F1 = compreal * F
now :: thesis: for c being object st c in dom F1 holds
F1 . c = (compreal * F) . c
let c be object ; :: thesis: ( c in dom F1 implies F1 . c = (compreal * F) . c )
assume A5: c in dom F1 ; :: thesis: F1 . c = (compreal * F) . c
thus F1 . c = - (F . c) by A4, VALUED_1:8
.= compreal . (F . c) by BINOP_2:def 7
.= (compreal * F) . c by A1, A4, A5, FUNCT_1:13 ; :: thesis: verum
end;
hence F1 = compreal * F by A3, A4, FUNCT_1:2, VALUED_1:8; :: thesis: verum
end;
assume A6: F1 = compreal * F ; :: thesis: F1 = - F
now :: thesis: for c being object st c in dom F1 holds
(- F) . c = (compreal * F) . c
let c be object ; :: thesis: ( c in dom F1 implies (- F) . c = (compreal * F) . c )
assume A7: c in dom F1 ; :: thesis: (- F) . c = (compreal * F) . c
thus (- F) . c = - (F . c) by VALUED_1:8
.= compreal . (F . c) by BINOP_2:def 7
.= (compreal * F) . c by A6, A7, FUNCT_1:12 ; :: thesis: verum
end;
hence F1 = - F by A1, A2, A6, FUNCT_1:2, RELAT_1:27; :: thesis: verum