let A be non empty set ; :: thesis: for f, g being Element of PFuncs A,REAL holds (multpfunc A) . f,g = (multpfunc A) . g,f
let f, g be Element of PFuncs A,REAL ; :: thesis: (multpfunc A) . f,g = (multpfunc A) . g,f
A1: dom ((multpfunc A) . g,f) = (dom g) /\ (dom f) by Th7;
A2: dom ((multpfunc A) . f,g) = (dom f) /\ (dom g) by Th7;

now

let x be Element of A; :: thesis: ( x in (dom f) /\ (dom g) implies ((multpfunc A) . f,g) . x = ((multpfunc A) . g,f) . x )
assume A3: x in (dom f) /\ (dom g) ; :: thesis: ((multpfunc A) . f,g) . x = ((multpfunc A) . g,f) . x
hence ((multpfunc A) . f,g) . x = (g . x) * (f . x) by A2, Th7
.= ((multpfunc A) . g,f) . x by A1, A3, Th7 ;
:: thesis: verum

end;

hence (multpfunc A) . f,g = (multpfunc A) . g,f by A2, A1, PARTFUN1:34; :: thesis: verum