let x1 be Element of REAL ; :: according to BINOP_1:def 20 :: thesis: for b₁ being Element of REAL holds sqrreal . (multreal . x1,b₁) = multreal . (sqrreal . x1),(sqrreal . b₁)
let x2 be Element of REAL ; :: thesis: sqrreal . (multreal . x1,x2) = multreal . (sqrreal . x1),(sqrreal . x2)
thus sqrreal . (multreal . x1,x2) = sqrreal . (x1 * x2) by BINOP_2:def 11
.= (x1 * x2) ^2 by Def2
.= (x1 ^2 ) * (x2 ^2 )
.= multreal . (x1 ^2 ),(x2 ^2 ) by BINOP_2:def 11
.= multreal . (sqrreal . x1),(x2 ^2 ) by Def2
.= multreal . (sqrreal . x1),(sqrreal . x2) by Def2 ; :: thesis: verum