let X1, X2 be set ; :: thesis: 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 ; :: thesis: 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; :: thesis: for f2 being PartFunc of X2,Y2 holds f1 <++> f2 = f2 <++> f1
let f2 be PartFunc of X2,Y2; :: thesis: f1 <++> f2 = f2 <++> f1
dom (f1 <++> f2) = (dom f1) /\ (dom f2) by Def45;
hence A1: dom (f1 <++> f2) = dom (f2 <++> f1) by Def45; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (f1 <++> f2) or (f1 <++> f2) . b₁ = (f2 <++> f1) . b₁ )
let x be object ; :: thesis: ( not x in dom (f1 <++> f2) or (f1 <++> f2) . x = (f2 <++> f1) . x )
assume A2: x in dom (f1 <++> f2) ; :: thesis: (f1 <++> f2) . x = (f2 <++> f1) . x
hence (f1 <++> f2) . x = (f1 . x) + (f2 . x) by Def45
.= (f2 <++> f1) . x by A1, A2, Def45 ;
:: thesis: verum