let i be Nat; :: thesis: for r being real number
for R being Element of i -tuples_on REAL holds sqr (r * R) = (r ^2 ) * (sqr R)
let r be real number ; :: thesis: for R being Element of i -tuples_on REAL holds sqr (r * R) = (r ^2 ) * (sqr R)
let R be Element of i -tuples_on REAL ; :: thesis: sqr (r * R) = (r ^2 ) * (sqr R)
A1: rng R c= REAL ;
A2: rng (sqrreal * R) c= REAL ;
reconsider s = r as Element of REAL by XREAL_0:def 1;
thus sqr (r * R) = sqrreal * (multreal [;] r,((id REAL ) * R)) by FUNCOP_1:44
.= sqrreal * (multreal [;] r,R) by A1, RELAT_1:79
.= multreal [;] (sqrreal . s),(sqrreal * R) by Th17, FINSEQOP:53
.= multreal [;] (sqrreal . r),((id REAL ) * (sqrreal * R)) by A2, RELAT_1:79
.= (multreal [;] (sqrreal . r),(id REAL )) * (sqrreal * R) by FUNCOP_1:44
.= (r ^2 ) * (sqr R) by Def2 ; :: thesis: verum