let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,COMPLEX holds (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
let f1, f2 be PartFunc of C,COMPLEX; :: thesis: (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^)
A1: dom ((f1 (#) f2) ^) = (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0c}) by Def2
.= ((dom f1) \ (f1 " {0c})) /\ ((dom f2) \ (f2 " {0c})) by Th7
.= (dom (f1 ^)) /\ ((dom f2) \ (f2 " {0c})) by Def2
.= (dom (f1 ^)) /\ (dom (f2 ^)) by Def2
.= dom ((f1 ^) (#) (f2 ^)) by Th3 ;

now :: thesis: for c being Element of C st c in dom ((f1 (#) f2) ^) holds
((f1 (#) f2) ^) /. c = ((f1 ^) (#) (f2 ^)) /. c

let c be Element of C; :: thesis: ( c in dom ((f1 (#) f2) ^) implies ((f1 (#) f2) ^) /. c = ((f1 ^) (#) (f2 ^)) /. c )
assume A2: c in dom ((f1 (#) f2) ^) ; :: thesis: ((f1 (#) f2) ^) /. c = ((f1 ^) (#) (f2 ^)) /. c
then c in (dom (f1 (#) f2)) \ ((f1 (#) f2) " {0c}) by Def2;
then A3: c in dom (f1 (#) f2) by XBOOLE_0:def 5;
A4: c in (dom (f1 ^)) /\ (dom (f2 ^)) by A1, A2, Th3;
then A5: c in dom (f1 ^) by XBOOLE_0:def 4;
A6: c in dom (f2 ^) by A4, XBOOLE_0:def 4;
thus ((f1 (#) f2) ^) /. c = ((f1 (#) f2) /. c) " by A2, Def2
.= ((f1 /. c) * (f2 /. c)) " by A3, Th3
.= ((f1 /. c) ") * ((f2 /. c) ") by XCMPLX_1:204
.= ((f1 ^) /. c) * ((f2 /. c) ") by A5, Def2
.= ((f1 ^) /. c) * ((f2 ^) /. c) by A6, Def2
.= ((f1 ^) (#) (f2 ^)) /. c by A1, A2, Th3 ; :: thesis: verum

end;

hence (f1 (#) f2) ^ = (f1 ^) (#) (f2 ^) by A1, PARTFUN2:1; :: thesis: verum