let F1 be FinSequence of COMPLEX ; :: thesis: ( F1 = c * F iff F1 = (c multcomplex) * F )
A1: dom (c * F) = dom F by VALUED_1:def 5;
A2: ( rng F c= COMPLEX & dom (c multcomplex) = COMPLEX ) by FUNCT_2:def 1;
then A3: dom ((c multcomplex) * F) = dom F by RELAT_1:27;
thus ( F1 = c * F implies F1 = (c multcomplex) * F ) :: thesis: ( F1 = (c multcomplex) * F implies F1 = c * F )

proof

assume A4: F1 = c * F ; :: thesis: F1 = (c multcomplex) * F

now :: thesis: for s being object st s in dom F1 holds
F1 . s = ((c multcomplex) * F) . s

let s be object ; :: thesis: ( s in dom F1 implies F1 . s = ((c multcomplex) * F) . s )
assume A5: s in dom F1 ; :: thesis: F1 . s = ((c multcomplex) * F) . s
hence F1 . s = c * (F . s) by A4, VALUED_1:def 5
.= (c multcomplex) . (F . s) by Lm1
.= ((c multcomplex) * F) . s by A1, A4, A5, FUNCT_1:13 ;
:: thesis: verum

end;

hence F1 = (c multcomplex) * F by A1, A3, A4, FUNCT_1:2; :: thesis: verum

end;

assume A6: F1 = (c multcomplex) * F ; :: thesis: F1 = c * F

now :: thesis: for s being object st s in dom F1 holds
(c * F) . s = ((c multcomplex) * F) . s

let s be object ; :: thesis: ( s in dom F1 implies (c * F) . s = ((c multcomplex) * F) . s )
assume A7: s in dom F1 ; :: thesis: (c * F) . s = ((c multcomplex) * F) . s
thus (c * F) . s = c * (F . s) by VALUED_1:6
.= (c multcomplex) . (F . s) by Lm1
.= ((c multcomplex) * F) . s by A6, A7, FUNCT_1:12 ; :: thesis: verum

end;

hence F1 = c * F by A1, A2, A6, FUNCT_1:2, RELAT_1:27; :: thesis: verum