let S1, S2, E be non empty ManySortedSign ; for f1, g1, f2, g2 being Function st f1 tolerates f2 & f1,g1 form_morphism_between S1,E & f2,g2 form_morphism_between S2,E holds
f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,E
let f1, g1, f2, g2 be Function; ( f1 tolerates f2 & f1,g1 form_morphism_between S1,E & f2,g2 form_morphism_between S2,E implies f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,E )
assume that
A1:
f1 tolerates f2
and
A2:
dom f1 = the carrier of S1
and
A3:
dom g1 = the carrier' of S1
and
A4:
rng f1 c= the carrier of E
and
A5:
rng g1 c= the carrier' of E
and
A6:
f1 * the ResultSort of S1 = the ResultSort of E * g1
and
A7:
for o being set
for p being Function st o in the carrier' of S1 & p = the Arity of S1 . o holds
f1 * p = the Arity of E . (g1 . o)
and
A8:
dom f2 = the carrier of S2
and
A9:
dom g2 = the carrier' of S2
and
A10:
rng f2 c= the carrier of E
and
A11:
rng g2 c= the carrier' of E
and
A12:
f2 * the ResultSort of S2 = the ResultSort of E * g2
and
A13:
for o being set
for p being Function st o in the carrier' of S2 & p = the Arity of S2 . o holds
f2 * p = the Arity of E . (g2 . o)
; PUA2MSS1:def 12 f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,E
set f = f1 +* f2;
set g = g1 +* g2;
set S = S1 +* S2;
the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2
by CIRCCOMB:def 2;
hence
dom (f1 +* f2) = the carrier of (S1 +* S2)
by A2, A8, FUNCT_4:def 1; PUA2MSS1:def 12 ( dom (g1 +* g2) = the carrier' of (S1 +* S2) & rng (f1 +* f2) c= the carrier of E & rng (g1 +* g2) c= the carrier' of E & the ResultSort of (S1 +* S2) * (f1 +* f2) = (g1 +* g2) * the ResultSort of E & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S1 +* S2) or not b2 = the Arity of (S1 +* S2) . b1 or b2 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . b1) ) ) )
A14:
the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2
by CIRCCOMB:def 2;
hence
dom (g1 +* g2) = the carrier' of (S1 +* S2)
by A3, A9, FUNCT_4:def 1; ( rng (f1 +* f2) c= the carrier of E & rng (g1 +* g2) c= the carrier' of E & the ResultSort of (S1 +* S2) * (f1 +* f2) = (g1 +* g2) * the ResultSort of E & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S1 +* S2) or not b2 = the Arity of (S1 +* S2) . b1 or b2 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . b1) ) ) )
A15:
rng (f1 +* f2) c= (rng f1) \/ (rng f2)
by FUNCT_4:17;
(rng f1) \/ (rng f2) c= the carrier of E
by A4, A10, XBOOLE_1:8;
hence
rng (f1 +* f2) c= the carrier of E
by A15; ( rng (g1 +* g2) c= the carrier' of E & the ResultSort of (S1 +* S2) * (f1 +* f2) = (g1 +* g2) * the ResultSort of E & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S1 +* S2) or not b2 = the Arity of (S1 +* S2) . b1 or b2 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . b1) ) ) )
A16:
rng (g1 +* g2) c= (rng g1) \/ (rng g2)
by FUNCT_4:17;
(rng g1) \/ (rng g2) c= the carrier' of E
by A5, A11, XBOOLE_1:8;
hence
rng (g1 +* g2) c= the carrier' of E
by A16; ( the ResultSort of (S1 +* S2) * (f1 +* f2) = (g1 +* g2) * the ResultSort of E & ( for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S1 +* S2) or not b2 = the Arity of (S1 +* S2) . b1 or b2 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . b1) ) ) )
A17:
rng the ResultSort of S1 c= the carrier of S1
;
A18:
rng the ResultSort of S2 c= the carrier of S2
;
A19:
dom the ResultSort of E = the carrier' of E
by FUNCT_2:def 1;
the ResultSort of S1 +* the ResultSort of S2 = the ResultSort of (S1 +* S2)
by CIRCCOMB:def 2;
hence (f1 +* f2) * the ResultSort of (S1 +* S2) =
(f1 * the ResultSort of S1) +* (f2 * the ResultSort of S2)
by A1, A2, A8, A17, A18, FUNCT_4:69
.=
the ResultSort of E * (g1 +* g2)
by A6, A11, A12, A19, FUNCT_7:9
;
for b1 being set
for b2 being set holds
( not b1 in the carrier' of (S1 +* S2) or not b2 = the Arity of (S1 +* S2) . b1 or b2 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . b1) )
let o be set ; for b1 being set holds
( not o in the carrier' of (S1 +* S2) or not b1 = the Arity of (S1 +* S2) . o or b1 * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o) )
let p be Function; ( not o in the carrier' of (S1 +* S2) or not p = the Arity of (S1 +* S2) . o or p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o) )
assume that
A20:
o in the carrier' of (S1 +* S2)
and
A21:
p = the Arity of (S1 +* S2) . o
; p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o)
A22:
the Arity of S1 +* the Arity of S2 = the Arity of (S1 +* S2)
by CIRCCOMB:def 2;
A23:
dom the Arity of S1 = the carrier' of S1
by FUNCT_2:def 1;
A24:
dom the Arity of S2 = the carrier' of S2
by FUNCT_2:def 1;
per cases
( o in the carrier' of S2 or not o in the carrier' of S2 )
;
suppose A25:
o in the
carrier' of
S2
;
p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o)then A26:
p = the
Arity of
S2 . o
by A21, A22, A24, FUNCT_4:13;
then
p in rng the
Arity of
S2
by A24, A25, FUNCT_1:def 3;
then
p is
FinSequence of the
carrier of
S2
by FINSEQ_1:def 11;
then
rng p c= dom f2
by A8, FINSEQ_1:def 4;
then A27:
dom (f2 * p) = dom p
by RELAT_1:27;
A28:
dom (f1 * p) c= dom p
by RELAT_1:25;
thus (f1 +* f2) * p =
(f1 * p) +* (f2 * p)
by FUNCT_7:10
.=
f2 * p
by A28, A27, FUNCT_4:19
.=
the
Arity of
E . (g2 . o)
by A13, A25, A26
.=
the
Arity of
E . ((g1 +* g2) . o)
by A9, A25, FUNCT_4:13
;
verum end; suppose A29:
not
o in the
carrier' of
S2
;
p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o)A30:
dom (f2 * p) c= dom p
by RELAT_1:25;
A31:
o in the
carrier' of
S1
by A14, A20, A29, XBOOLE_0:def 3;
A32:
p = the
Arity of
S1 . o
by A21, A22, A24, A29, FUNCT_4:11;
then
p in rng the
Arity of
S1
by A23, A31, FUNCT_1:def 3;
then
p is
FinSequence of the
carrier of
S1
by FINSEQ_1:def 11;
then
rng p c= dom f1
by A2, FINSEQ_1:def 4;
then A33:
dom (f1 * p) = dom p
by RELAT_1:27;
thus (f1 +* f2) * p =
(f2 +* f1) * p
by A1, FUNCT_4:34
.=
(f2 * p) +* (f1 * p)
by FUNCT_7:10
.=
f1 * p
by A33, A30, FUNCT_4:19
.=
the
Arity of
E . (g1 . o)
by A7, A31, A32
.=
the
Arity of
E . ((g1 +* g2) . o)
by A9, A29, FUNCT_4:11
;
verum end;