let C be non empty set ; :: thesis: for f1, f2 being PartFunc of C,ExtREAL holds f1 (#) f2 = f2 (#) f1
let f1, f2 be PartFunc of C,ExtREAL ; :: thesis: f1 (#) f2 = f2 (#) f1
A1: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by Def5
.= dom (f2 (#) f1) by Def5 ;
for x being Element of C st x in dom (f1 (#) f2) holds
(f1 (#) f2) . x = (f2 (#) f1) . x

proof

let x be Element of C; :: thesis: ( x in dom (f1 (#) f2) implies (f1 (#) f2) . x = (f2 (#) f1) . x )
assume A2: x in dom (f1 (#) f2) ; :: thesis: (f1 (#) f2) . x = (f2 (#) f1) . x
then (f1 (#) f2) . x = (f1 . x) * (f2 . x) by Def5;
hence (f1 (#) f2) . x = (f2 (#) f1) . x by A1, A2, Def5; :: thesis: verum

end;

hence f1 (#) f2 = f2 (#) f1 by A1, PARTFUN1:34; :: thesis: verum