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)))
A1: multreal .: (f,(addreal .: (g,h))) = addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))
proof
let a be Element of A; :: according to FUNCT_2:def 8 :: 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
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:37
.= multreal . ((f . b),(addreal . ((g . b),(h . b)))) by FUNCOP_1:37
.= (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:37
.= addreal . (((multreal .: (ff,g)) . a),((multreal .: (ff,h)) . a)) by FUNCOP_1:37
.= (addreal .: ((multreal .: (f,g)),(multreal .: (f,h)))) . a by FUNCOP_1:37 ; :: thesis: verum
end;
end;
end;
thus (RealFuncMult A) . (f,((RealFuncAdd A) . (g,h))) = (RealFuncMult A) . (f,(addreal .: (g,h))) by Def1
.= addreal .: ((multreal .: (f,g)),(multreal .: (f,h))) by A1, Def2
.= (RealFuncAdd A) . ((multreal .: (f,g)),(multreal .: (f,h))) by Def1
.= (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),(multreal .: (f,h))) by Def2
.= (RealFuncAdd A) . (((RealFuncMult A) . (f,g)),((RealFuncMult A) . (f,h))) by Def2 ; :: thesis: verum