let A be set ; :: thesis: for f, g, h being Element of Funcs A,REAL holds (RealFuncMult A) . f,((RealFuncAdd A) . g,h) = (RealFuncAdd A) . ((RealFuncMult A) . f,g),((RealFuncMult A) . f,h)
let f, g, h be Element of Funcs A,REAL ; :: thesis: (RealFuncMult A) . f,((RealFuncAdd A) . g,h) = (RealFuncAdd A) . ((RealFuncMult A) . f,g),((RealFuncMult A) . f,h)
A: multreal .: f,(addreal .: g,h) = addreal .: (multreal .: f,g),(multreal .: f,h)

proof

let a be Element of A; :: according to FUNCT_2:def 9 :: thesis: (multreal .: f,(addreal .: g,h)) . a = (addreal .: (multreal .: f,g),(multreal .: f,h)) . a

per cases ( A = {} or A <> {} ) ;

suppose A = {} ; :: thesis: (multreal .: f,(addreal .: g,h)) . a = (addreal .: (multreal .: f,g),(multreal .: f,h)) . a

then f = {} ;
hence (multreal .: f,(addreal .: g,h)) . a = (addreal .: (multreal .: f,g),(multreal .: f,h)) . a ; :: thesis: verum

end;

suppose A <> {} ; :: thesis: (multreal .: f,(addreal .: g,h)) . a = (addreal .: (multreal .: f,g),(multreal .: f,h)) . a

then reconsider B = A as non empty set ;
reconsider ff = f, gg = g, hh = h as Element of Funcs B,REAL ;
reconsider b = a as Element of B ;
thus (multreal .: f,(addreal .: g,h)) . a = multreal . (f . b),((addreal .: g,h) . b) by FUNCOP_1:48
.= multreal . (f . b),(addreal . (g . b),(h . b)) by FUNCOP_1:48
.= (ff . b) * (addreal . (gg . b),(hh . b)) by BINOP_2:def 11
.= (ff . b) * ((gg . b) + (hh . b)) by BINOP_2:def 9
.= ((ff . b) * (gg . b)) + ((ff . b) * (hh . b))
.= ((ff . b) * (gg . b)) + (multreal . (ff . b),(hh . b)) by BINOP_2:def 11
.= (multreal . (ff . b),(gg . b)) + (multreal . (ff . b),(hh . b)) by BINOP_2:def 11
.= addreal . (multreal . (f . a),(g . a)),(multreal . (f . a),(h . a)) by BINOP_2:def 9
.= addreal . (multreal . (f . a),(g . a)),((multreal .: ff,h) . a) by FUNCOP_1:48
.= addreal . ((multreal .: ff,g) . a),((multreal .: ff,h) . a) by FUNCOP_1:48
.= (addreal .: (multreal .: f,g),(multreal .: f,h)) . a by FUNCOP_1:48 ; :: thesis: verum

end;

end;

end;

thus (RealFuncMult A) . f,((RealFuncAdd A) . g,h) = (RealFuncMult A) . f,(addreal .: g,h) by Def2
.= multreal .: f,(addreal .: g,h) by Def3
.= addreal .: (multreal .: f,g),(multreal .: f,h) by A
.= (RealFuncAdd A) . (multreal .: f,g),(multreal .: f,h) by Def2
.= (RealFuncAdd A) . ((RealFuncMult A) . f,g),(multreal .: f,h) by Def3
.= (RealFuncAdd A) . ((RealFuncMult A) . f,g),((RealFuncMult A) . f,h) by Def3 ; :: thesis: verum