let R be FinSequence of REAL ; :: 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} )
assume A1: r <> 0 ; :: thesis: R " {(s / r)} = (r * R) " {s}
A2: ( Seg (len R) = dom R & dom (r * R) = Seg (len (r * R)) ) by FINSEQ_1:def 3;
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 set ; :: 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 reconsider i = x as Element of NAT ;
A4: ( i in dom R & R . i in {(s / r)} ) by A3, FUNCT_1:def 13;
then A5: ( i in Seg (len (r * R)) & R . i = s / r ) by A2, FINSEQ_2:37, TARSKI:def 1;
A6: i in dom (r * R) by A2, A4, FINSEQ_2:37;
r * (R . i) = s by A1, A5, XCMPLX_1:88;
then (r * R) . i = s by RVSUM_1:66;
then (r * R) . i in {s} by TARSKI:def 1;
hence x in (r * R) " {s} by A6, FUNCT_1:def 13; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (r * R) " {s} or x in R " {(s / r)} )
assume A7: x in (r * R) " {s} ; :: thesis: x in R " {(s / r)}
then reconsider i = x as Element of NAT ;
( i in dom (r * R) & (r * R) . i in {s} ) by A7, FUNCT_1:def 13;
then A8: ( i in dom R & (r * R) . i = s ) by A2, FINSEQ_2:37, TARSKI:def 1;
then r * (R . i) = s by RVSUM_1:66;
then R . i = s / r by A1, XCMPLX_1:90;
then R . i in {(s / r)} by TARSKI:def 1;
hence x in R " {(s / r)} by A8, FUNCT_1:def 13; :: thesis: verum