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 :: thesis: for x being Element of A st x in (dom f) /\ (dom g) holds
((multpfunc A) . (f,g)) . x = ((multpfunc A) . (g,f)) . x

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:5; :: thesis: verum