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)}

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 R by A1, FINSEQ_2:33;

hence x in R " {(s / r)} by A6, FUNCT_1:def 7; :: thesis: verum

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 * R) " {s} or x in R " {(s / r)} )
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 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 * R) by A1, FINSEQ_2:33;

hence x in (r * R) " {s} by A4, FUNCT_1:def 7; :: thesis: verum

end;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 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 * R) by A1, FINSEQ_2:33;

hence x in (r * R) " {s} by A4, FUNCT_1:def 7; :: thesis: verum

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 R by A1, FINSEQ_2:33;

hence x in R " {(s / r)} by A6, FUNCT_1:def 7; :: thesis: verum