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 ;
A2: 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 A3: x in dom (f1 (#) f2) ; :: thesis: (f1 (#) f2) . x = (f2 (#) f1) . x
A4: (f1 (#) f2) . x = (f1 . x) * (f2 . x) by A3, Def5;
thus (f1 (#) f2) . x = (f2 (#) f1) . x by A1, A3, A4, Def5; :: thesis: verum

end;

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