let p, q be Tuple of 1, REAL ; :: thesis: for r being Real st p = r * q & p <> <*0*> holds
ex a, b being Real st
( p = <*a*> & q = <*b*> & r = a / b )
let r be Real; :: thesis: ( p = r * q & p <> <*0*> implies ex a, b being Real st
( p = <*a*> & q = <*b*> & r = a / b ) )
assume that
A1: p = r * q and
A2: p <> <*0*> ; :: thesis: ex a, b being Real st
( p = <*a*> & q = <*b*> & r = a / b )
consider r1 being Element of REAL such that
A3: p = <*r1*> by FINSEQ_2:97;
consider r2 being Element of REAL such that
A4: q = <*r2*> by FINSEQ_2:97;
reconsider r1 = r1, r2 = r2 as Real ;
take r1 ; :: thesis: ex b being Real st
( p = <*r1*> & q = <*b*> & r = r1 / b )
take r2 ; :: thesis: ( p = <*r1*> & q = <*r2*> & r = r1 / r2 )
A5: <*r1*> = <*(r * r2)*> by A1, A3, A4, RVSUM_1:47;
then A6: r1 = r * r2 by FINSEQ_1:76;

per cases ( r2 = 0 or r2 <> 0 ) ;

suppose r2 = 0 ; :: thesis: ( p = <*r1*> & q = <*r2*> & r = r1 / r2 )

hence ( p = <*r1*> & q = <*r2*> & r = r1 / r2 ) by A5, A2, A3; :: thesis: verum

end;

suppose A7: r2 <> 0 ; :: thesis: ( p = <*r1*> & q = <*r2*> & r = r1 / r2 )

r = r * 1
.= r * (r2 / r2) by A7, XCMPLX_1:60
.= r1 / r2 by A6 ;
hence ( p = <*r1*> & q = <*r2*> & r = r1 / r2 ) by A3, A4; :: thesis: verum

end;

end;