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

proof

assume A4: F1 = r * F ; :: thesis: F1 = (r multreal) * F

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

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

end;

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

end;

assume A6: F1 = (r multreal) * F ; :: thesis: F1 = r * F

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

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

end;

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