let a be set ; 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; ( h = f \/ g implies (commute h) . a = ((commute f) . a) \/ ((commute g) . a) )
assume A1:
h = f \/ g
; (commute h) . a = ((commute f) . a) \/ ((commute g) . a)
now for u, v being object holds
( ( [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 [u,v] in (commute h) . a ) )let u,
v be
object ;
( ( [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 [b1,b2] in (commute h) . a ) )hereby ( [u,v] in ((commute f) . a) \/ ((commute g) . a) implies [b1,b2] in (commute h) . a )
assume A2:
[u,v] in (commute h) . a
;
[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;
verum
end; assume A8:
[u,v] in ((commute f) . a) \/ ((commute g) . a)
;
[b1,b2] in (commute h) . aper 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
;
[b1,b2] in (commute h) . athen 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;
verum end; suppose A19:
[u,v] in (commute g) . a
;
[b1,b2] in (commute h) . athen 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;
verum end; end;
hence
(commute h) . a = ((commute f) . a) \/ ((commute g) . a)
; verum