let a be set ; :: thesis: for f, g, h being Function st h = f \/ g holds
(commute h) . a = ((commute f) . a) \/ ((commute g) . a)
let f, g, h be Function; :: thesis: ( h = f \/ g implies (commute h) . a = ((commute f) . a) \/ ((commute g) . a) )
assume A1: h = f \/ g ; :: thesis: (commute h) . a = ((commute f) . a) \/ ((commute g) . a)

now

let u, v be set ; :: thesis: ( ( [u,v] in (commute h) . a implies [u,v] in ((commute f) . a) \/ ((commute g) . a) ) & ( [u,v] in ((commute f) . a) \/ ((commute g) . a) implies [b₁,b₂] in (commute h) . a ) )

hereby :: thesis: ( [u,v] in ((commute f) . a) \/ ((commute g) . a) implies [b₁,b₂] in (commute h) . a )

assume A2: [u,v] in (commute h) . a ; :: thesis: [u,v] in ((commute f) . a) \/ ((commute g) . a)
then A3: ((commute h) . a) . u = v by FUNCT_1:1;
u in dom ((commute h) . a) by A2, FUNCT_1:1;
then consider k being Function such that
A4: u in dom h and
A5: k = h . u and
A6: a in dom k by Th5;
[u,k] in h by A4, A5, FUNCT_1:def 2;
then ( [u,k] in f or [u,k] in g ) by A1, XBOOLE_0:def 3;
then ( ( u in dom f & k = f . u ) or ( u in dom g & k = g . u ) ) by FUNCT_1:1;
then A7: ( ( u in dom ((commute f) . a) & ((commute f) . a) . u = k . a ) or ( u in dom ((commute g) . a) & ((commute g) . a) . u = k . a ) ) by A6, Th5, Th6;
((commute h) . a) . u = k . a by A4, A5, A6, Th6;
then ( [u,v] in (commute f) . a or [u,v] in (commute g) . a ) by A7, A3, FUNCT_1:1;
hence [u,v] in ((commute f) . a) \/ ((commute g) . a) by XBOOLE_0:def 3; :: thesis: verum

end;

assume A8: [u,v] in ((commute f) . a) \/ ((commute g) . a) ; :: thesis: [b₁,b₂] in (commute h) . a

per cases ( [u,v] in (commute f) . a or [u,v] in (commute g) . a ) by A8, XBOOLE_0:def 3;

suppose A9: [u,v] in (commute f) . a ; :: thesis: [b₁,b₂] in (commute h) . a

then A10: ((commute f) . a) . u = v by FUNCT_1:1;
u in dom ((commute f) . a) by A9, FUNCT_1:1;
then consider k being Function such that
A11: u in dom f and
A12: k = f . u and
A13: a in dom k by Th5;
A14: ((commute f) . a) . u = k . a by A11, A12, A13, Th6;
[u,k] in f by A11, A12, FUNCT_1:1;
then A15: [u,k] in h by A1, XBOOLE_0:def 3;
then A16: u in dom h by FUNCT_1:1;
A17: k = h . u by A15, FUNCT_1:1;
then A18: ((commute h) . a) . u = k . a by A16, A13, Th6;
u in dom ((commute h) . a) by A16, A17, A13, Th5;
hence [u,v] in (commute h) . a by A18, A14, A10, FUNCT_1:1; :: thesis: verum

end;

suppose A19: [u,v] in (commute g) . a ; :: thesis: [b₁,b₂] in (commute h) . a

then A20: ((commute g) . a) . u = v by FUNCT_1:1;
u in dom ((commute g) . a) by A19, FUNCT_1:1;
then consider k being Function such that
A21: u in dom g and
A22: k = g . u and
A23: a in dom k by Th5;
A24: ((commute g) . a) . u = k . a by A21, A22, A23, Th6;
[u,k] in g by A21, A22, FUNCT_1:1;
then A25: [u,k] in h by A1, XBOOLE_0:def 3;
then A26: u in dom h by FUNCT_1:1;
A27: k = h . u by A25, FUNCT_1:1;
then A28: ((commute h) . a) . u = k . a by A26, A23, Th6;
u in dom ((commute h) . a) by A26, A27, A23, Th5;
hence [u,v] in (commute h) . a by A28, A24, A20, FUNCT_1:1; :: thesis: verum

end;

end;

end;

hence (commute h) . a = ((commute f) . a) \/ ((commute g) . a) by RELAT_1:def 2; :: thesis: verum