thus multcpfunc A is commutative :: thesis: multcpfunc A is associative

proof

let f, g be Element of PFuncs (A,COMPLEX); :: according to BINOP_1:def 2 :: thesis: (multcpfunc A) . (f,g) = (multcpfunc A) . (g,f)
A1: dom ((multcpfunc A) . (g,f)) = (dom g) /\ (dom f) by Th5;
A2: dom ((multcpfunc A) . (f,g)) = (dom f) /\ (dom g) by Th5;

now :: thesis: for x being Element of A st x in (dom f) /\ (dom g) holds
((multcpfunc A) . (f,g)) . x = ((multcpfunc A) . (g,f)) . x

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

end;

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

end;

let f, g, h be Element of PFuncs (A,COMPLEX); :: according to BINOP_1:def 3 :: thesis: (multcpfunc A) . (f,((multcpfunc A) . (g,h))) = (multcpfunc A) . (((multcpfunc A) . (f,g)),h)
set j = (multcpfunc A) . (g,h);
set k = (multcpfunc A) . (f,g);
set j1 = (multcpfunc A) . (f,((multcpfunc A) . (g,h)));
set k1 = (multcpfunc A) . (((multcpfunc A) . (f,g)),h);
A4: dom ((multcpfunc A) . (((multcpfunc A) . (f,g)),h)) = (dom ((multcpfunc A) . (f,g))) /\ (dom h) by Th5;
then A5: dom ((multcpfunc A) . (((multcpfunc A) . (f,g)),h)) c= dom ((multcpfunc A) . (f,g)) by XBOOLE_1:17;
A6: dom ((multcpfunc A) . (((multcpfunc A) . (f,g)),h)) = ((dom f) /\ (dom g)) /\ (dom h) by A4, Th5;
A7: dom ((multcpfunc A) . (f,((multcpfunc A) . (g,h)))) = (dom f) /\ (dom ((multcpfunc A) . (g,h))) by Th5;
then A8: dom ((multcpfunc A) . (f,((multcpfunc A) . (g,h)))) = (dom f) /\ ((dom g) /\ (dom h)) by Th5;
A9: dom ((multcpfunc A) . (f,((multcpfunc A) . (g,h)))) c= dom ((multcpfunc A) . (g,h)) by A7, XBOOLE_1:17;

now :: thesis: for x being Element of A st x in dom ((multcpfunc A) . (f,((multcpfunc A) . (g,h)))) holds
((multcpfunc A) . (f,((multcpfunc A) . (g,h)))) . x = ((multcpfunc A) . (((multcpfunc A) . (f,g)),h)) . x

let x be Element of A; :: thesis: ( x in dom ((multcpfunc A) . (f,((multcpfunc A) . (g,h)))) implies ((multcpfunc A) . (f,((multcpfunc A) . (g,h)))) . x = ((multcpfunc A) . (((multcpfunc A) . (f,g)),h)) . x )
assume A10: x in dom ((multcpfunc A) . (f,((multcpfunc A) . (g,h)))) ; :: thesis: ((multcpfunc A) . (f,((multcpfunc A) . (g,h)))) . x = ((multcpfunc A) . (((multcpfunc A) . (f,g)),h)) . x
then A11: x in dom ((multcpfunc A) . (((multcpfunc A) . (f,g)),h)) by A8, A6, XBOOLE_1:16;
thus ((multcpfunc A) . (f,((multcpfunc A) . (g,h)))) . x = (f . x) * (((multcpfunc A) . (g,h)) . x) by A10, Th5
.= (f . x) * ((g . x) * (h . x)) by A9, A10, Th5
.= ((f . x) * (g . x)) * (h . x)
.= (((multcpfunc A) . (f,g)) . x) * (h . x) by A5, A11, Th5
.= ((multcpfunc A) . (((multcpfunc A) . (f,g)),h)) . x by A11, Th5 ; :: thesis: verum

end;

hence (multcpfunc A) . (f,((multcpfunc A) . (g,h))) = (multcpfunc A) . (((multcpfunc A) . (f,g)),h) by A8, A6, PARTFUN1:5, XBOOLE_1:16; :: thesis: verum