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} )
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}
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 reconsider i = x as Element of NAT ;
R . i in {(s / r)} by ;
then R . i = s / r by TARSKI:def 1;
then r * (R . i) = s by ;
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 ;
then i in dom (r * R) by ;
hence x in (r * R) " {s} by ; :: 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 ;
then (r * R) . i = s by TARSKI:def 1;
then r * (R . i) = s by RVSUM_1:44;
then R . i = s / r by ;
then A6: R . i in {(s / r)} by TARSKI:def 1;
i in dom (r * R) by ;
then i in dom R by ;
hence x in R " {(s / r)} by ; :: thesis: verum