let X1, X2 be set ; for Y1, Y2 being complex-functions-membered set
for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds f1 <##> f2 = f2 <##> f1
let Y1, Y2 be complex-functions-membered set ; for f1 being PartFunc of X1,Y1
for f2 being PartFunc of X2,Y2 holds f1 <##> f2 = f2 <##> f1
let f1 be PartFunc of X1,Y1; for f2 being PartFunc of X2,Y2 holds f1 <##> f2 = f2 <##> f1
let f2 be PartFunc of X2,Y2; f1 <##> f2 = f2 <##> f1
dom (f1 <##> f2) = (dom f1) /\ (dom f2)
by Def47;
hence A1:
dom (f1 <##> f2) = dom (f2 <##> f1)
by Def47; FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (f1 <##> f2) or (f1 <##> f2) . b1 = (f2 <##> f1) . b1 )
let x be object ; ( not x in dom (f1 <##> f2) or (f1 <##> f2) . x = (f2 <##> f1) . x )
assume A2:
x in dom (f1 <##> f2)
; (f1 <##> f2) . x = (f2 <##> f1) . x
hence (f1 <##> f2) . x =
(f1 . x) (#) (f2 . x)
by Def47
.=
(f2 <##> f1) . x
by A1, A2, Def47
;
verum