let A be non empty set ; for f, g, h being Element of PFuncs A,REAL holds (multpfunc A) . f,((addpfunc A) . g,h) = (addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)
let f, g, h be Element of PFuncs A,REAL ; (multpfunc A) . f,((addpfunc A) . g,h) = (addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)
set i = (multpfunc A) . f,h;
set j = (multpfunc A) . f,g;
set k = (addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h);
set l = (addpfunc A) . g,h;
set m = (multpfunc A) . f,((addpfunc A) . g,h);
A1:
((dom f) /\ (dom g)) /\ (dom h) = (dom f) /\ ((dom g) /\ (dom h))
by XBOOLE_1:16;
( dom ((multpfunc A) . f,h) = (dom f) /\ (dom h) & dom ((multpfunc A) . f,g) = (dom f) /\ (dom g) )
by Th7;
then
dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) = ((dom h) /\ (dom f)) /\ ((dom f) /\ (dom g))
by Th6;
then
dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) = (dom h) /\ ((dom f) /\ ((dom f) /\ (dom g)))
by XBOOLE_1:16;
then A2:
dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) = (dom h) /\ (((dom f) /\ (dom f)) /\ (dom g))
by XBOOLE_1:16;
A3:
((dom f) /\ (dom g)) /\ (dom h) = (dom g) /\ ((dom f) /\ (dom h))
by XBOOLE_1:16;
A4:
now let x be
Element of
A;
( x in dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) implies ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = ((multpfunc A) . f,((addpfunc A) . g,h)) . x )assume A5:
x in dom ((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h))
;
((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = ((multpfunc A) . f,((addpfunc A) . g,h)) . xthen
x in (dom f) /\ (dom g)
by A2, XBOOLE_0:def 4;
then A6:
x in dom (f (#) g)
by VALUED_1:def 4;
x in (dom g) /\ (dom h)
by A2, A1, A5, XBOOLE_0:def 4;
then A7:
x in dom (g + h)
by VALUED_1:def 1;
((multpfunc A) . f,g) . x = (f (#) g) . x
by Def3;
then A8:
((multpfunc A) . f,g) . x = (f . x) * (g . x)
by A6, VALUED_1:def 4;
x in (dom f) /\ (dom h)
by A2, A3, A5, XBOOLE_0:def 4;
then A9:
x in dom (f (#) h)
by VALUED_1:def 4;
((multpfunc A) . f,h) . x = (f (#) h) . x
by Def3;
then A10:
((multpfunc A) . f,h) . x = (f . x) * (h . x)
by A9, VALUED_1:def 4;
((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = (((multpfunc A) . f,g) . x) + (((multpfunc A) . f,h) . x)
by A5, Th6;
then
(
((addpfunc A) . g,h) . x = (g + h) . x &
((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = (f . x) * ((g . x) + (h . x)) )
by A8, A10, RFUNCT_3:def 4;
then A11:
((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = (f . x) * (((addpfunc A) . g,h) . x)
by A7, VALUED_1:def 1;
x in (dom f) /\ (dom ((addpfunc A) . g,h))
by A2, A1, A5, Th6;
then A12:
x in dom (f (#) ((addpfunc A) . g,h))
by VALUED_1:def 4;
((multpfunc A) . f,((addpfunc A) . g,h)) . x = (f (#) ((addpfunc A) . g,h)) . x
by Def3;
hence
((addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)) . x = ((multpfunc A) . f,((addpfunc A) . g,h)) . x
by A12, A11, VALUED_1:def 4;
verum end;
( dom ((multpfunc A) . f,((addpfunc A) . g,h)) = (dom f) /\ (dom ((addpfunc A) . g,h)) & dom ((addpfunc A) . g,h) = (dom g) /\ (dom h) )
by Th6, Th7;
hence
(multpfunc A) . f,((addpfunc A) . g,h) = (addpfunc A) . ((multpfunc A) . f,g),((multpfunc A) . f,h)
by A2, A4, PARTFUN1:34, XBOOLE_1:16; verum