let R be real-valued FinSequence; :: thesis: for r, s being Real st r <> 0 holds
R " {(s / r)} = (r * R) " {s}
let r, s be Real; :: thesis: ( r <> 0 implies R " {(s / r)} = (r * R) " {s} )
A1: ( Seg (len R) = dom R & dom (r * R) = Seg (len (r * R)) ) by FINSEQ_1:def 3;
assume A2: r <> 0 ; :: thesis: R " {(s / r)} = (r * R) " {s}
reconsider R1 = R as FinSequence of REAL by RVSUM_1:145;
thus R " {(s / r)} c= (r * R) " {s} :: according to XBOOLE_0:def 10 :: thesis: (r * R) " {s} c= R " {(s / r)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R " {(s / r)} or x in (r * R) " {s} )
assume A3: x in R " {(s / r)} ; :: thesis: x in (r * R) " {s}
then x in R1 " {(s / r)} ;
then reconsider i = x as Element of NAT ;
R . i in {(s / r)} by A3, FUNCT_1:def 7;
then R . i = s / r by TARSKI:def 1;
then r * (R . i) = s by A2, XCMPLX_1:87;
then (r * R) . i = s by RVSUM_1:44;
then A4: (r * R) . i in {s} by TARSKI:def 1;
i in dom R by A3, FUNCT_1:def 7;
then i in dom (r * R1) by A1, FINSEQ_2:33;
hence x in (r * R) " {s} by A4, FUNCT_1:def 7; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (r * R) " {s} or x in R " {(s / r)} )
assume A5: x in (r * R) " {s} ; :: thesis: x in R " {(s / r)}
then reconsider i = x as Element of NAT ;
(r * R) . i in {s} by A5, FUNCT_1:def 7;
then (r * R) . i = s by TARSKI:def 1;
then r * (R . i) = s by RVSUM_1:44;
then R . i = s / r by A2, XCMPLX_1:89;
then A6: R . i in {(s / r)} by TARSKI:def 1;
i in dom (r * R) by A5, FUNCT_1:def 7;
then i in dom R1 by A1, FINSEQ_2:33;
hence x in R " {(s / r)} by A6, FUNCT_1:def 7; :: thesis: verum