let a be Real; for A being non empty set
for f, g being Element of PFuncs A,REAL holds (addpfunc A) . ((multrealpfunc A) . a,f),((multrealpfunc A) . a,g) = (multrealpfunc A) . a,((addpfunc A) . f,g)
let A be non empty set ; for f, g being Element of PFuncs A,REAL holds (addpfunc A) . ((multrealpfunc A) . a,f),((multrealpfunc A) . a,g) = (multrealpfunc A) . a,((addpfunc A) . f,g)
let f, g be Element of PFuncs A,REAL ; (addpfunc A) . ((multrealpfunc A) . a,f),((multrealpfunc A) . a,g) = (multrealpfunc A) . a,((addpfunc A) . f,g)
reconsider h = (multrealpfunc A) . a,f as Element of PFuncs A,REAL ;
reconsider i = (multrealpfunc A) . a,g as Element of PFuncs A,REAL ;
set j = (addpfunc A) . f,g;
reconsider k = (multrealpfunc A) . a,((addpfunc A) . f,g) as Element of PFuncs A,REAL ;
set l = (addpfunc A) . h,i;
A1:
( dom h = dom f & dom i = dom g )
by Th9;
A2:
dom ((addpfunc A) . h,i) = (dom h) /\ (dom i)
by Th6;
A3:
dom ((addpfunc A) . f,g) = (dom f) /\ (dom g)
by Th6;
A4:
now let x be
Element of
A;
( x in dom ((addpfunc A) . h,i) implies ((addpfunc A) . h,i) . x = k . x )A5:
h . x = (a (#) f) . x
by Def4;
assume A6:
x in dom ((addpfunc A) . h,i)
;
((addpfunc A) . h,i) . x = k . xthen A7:
x in dom (f + g)
by A1, A2, VALUED_1:def 1;
A8:
i . x = (a (#) g) . x
by Def4;
x in dom i
by A2, A6, XBOOLE_0:def 4;
then
x in dom g
by Th9;
then
x in dom (a (#) g)
by VALUED_1:def 5;
then A9:
i . x = a * (g . x)
by A8, VALUED_1:def 5;
x in dom h
by A2, A6, XBOOLE_0:def 4;
then
x in dom f
by Th9;
then
x in dom (a (#) f)
by VALUED_1:def 5;
then A10:
h . x = a * (f . x)
by A5, VALUED_1:def 5;
thus ((addpfunc A) . h,i) . x =
(h . x) + (i . x)
by A6, Th6
.=
a * ((f . x) + (g . x))
by A10, A9
.=
a * ((f + g) . x)
by A7, VALUED_1:def 1
.=
a * (((addpfunc A) . f,g) . x)
by RFUNCT_3:def 4
.=
k . x
by A1, A3, A2, A6, Th9
;
verum end;
dom k = dom ((addpfunc A) . f,g)
by Th9;
hence
(addpfunc A) . ((multrealpfunc A) . a,f),((multrealpfunc A) . a,g) = (multrealpfunc A) . a,((addpfunc A) . f,g)
by A1, A3, A2, A4, PARTFUN1:34; verum