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;