let x1, x2 be Element of REAL ; :: according to BINOP_1:def 20 :: 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