let S1, S2, E be non empty ManySortedSign ; :: thesis: 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; :: thesis: ( 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 & dom g1 = the carrier' of S1 )
and
A3:
rng f1 c= the carrier of E
and
B3:
rng g1 c= the carrier' of E
and
A4:
f1 * the ResultSort of S1 = the ResultSort of E * g1
and
A5:
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
A6:
( dom f2 = the carrier of S2 & dom g2 = the carrier' of S2 )
and
A7:
( rng f2 c= the carrier of E & rng g2 c= the carrier' of E )
and
A8:
f2 * the ResultSort of S2 = the ResultSort of E * g2
and
A9:
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)
; :: according to PUA2MSS1:def 13 :: thesis: 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, A6, FUNCT_4:def 1; :: according to PUA2MSS1:def 13 :: thesis: ( 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) ) ) )
A10:
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 A2, A6, FUNCT_4:def 1; :: thesis: ( 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) ) ) )
A11:
the ResultSort of S1 +* the ResultSort of S2 = the ResultSort of (S1 +* S2)
by CIRCCOMB:def 2;
( rng (f1 +* f2) c= (rng f1) \/ (rng f2) & (rng f1) \/ (rng f2) c= the carrier of E )
by A3, A7, FUNCT_4:18, XBOOLE_1:8;
hence
rng (f1 +* f2) c= the carrier of E
by XBOOLE_1:1; :: thesis: ( 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) ) ) )
( rng (g1 +* g2) c= (rng g1) \/ (rng g2) & (rng g1) \/ (rng g2) c= the carrier' of E )
by B3, A7, FUNCT_4:18, XBOOLE_1:8;
hence
rng (g1 +* g2) c= the carrier' of E
by XBOOLE_1:1; :: thesis: ( 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) ) ) )
A12:
( rng the ResultSort of S1 c= the carrier of S1 & rng the ResultSort of S2 c= the carrier of S2 )
;
A13:
dom the ResultSort of E = the carrier' of E
by FUNCT_2:def 1;
thus (f1 +* f2) * the ResultSort of (S1 +* S2) =
(f1 * the ResultSort of S1) +* (f2 * the ResultSort of S2)
by A1, A2, A6, A11, A12, FUNCT_4:73
.=
the ResultSort of E * (g1 +* g2)
by A4, A7, A8, A13, FUNCT_7:10
; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 A14:
( o in the carrier' of (S1 +* S2) & p = the Arity of (S1 +* S2) . o )
; :: thesis: p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o)
A15:
the Arity of S1 +* the Arity of S2 = the Arity of (S1 +* S2)
by CIRCCOMB:def 2;
A16:
( dom the Arity of S1 = the carrier' of S1 & rng the Arity of S1 c= the carrier of S1 * & dom the Arity of S2 = the carrier' of S2 & rng the Arity of S2 c= 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 A17:
o in the
carrier' of
S2
;
:: thesis: p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o)then A18:
p = the
Arity of
S2 . o
by A14, A15, A16, FUNCT_4:14;
then
p in rng the
Arity of
S2
by A16, A17, FUNCT_1:def 5;
then
p is
FinSequence of the
carrier of
S2
by FINSEQ_1:def 11;
then
rng p c= dom f2
by A6, FINSEQ_1:def 4;
then A19:
(
dom (f1 * p) c= dom p &
dom (f2 * p) = dom p )
by RELAT_1:44, RELAT_1:46;
thus (f1 +* f2) * p =
(f1 * p) +* (f2 * p)
by FUNCT_7:11
.=
f2 * p
by A19, FUNCT_4:20
.=
the
Arity of
E . (g2 . o)
by A9, A17, A18
.=
the
Arity of
E . ((g1 +* g2) . o)
by A6, A17, FUNCT_4:14
;
:: thesis: verum end; suppose A20:
not
o in the
carrier' of
S2
;
:: thesis: p * (f1 +* f2) = the Arity of E . ((g1 +* g2) . o)then A21:
o in the
carrier' of
S1
by A10, A14, XBOOLE_0:def 3;
A22:
p = the
Arity of
S1 . o
by A14, A15, A16, A20, FUNCT_4:12;
then
p in rng the
Arity of
S1
by A16, A21, FUNCT_1:def 5;
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 A23:
(
dom (f1 * p) = dom p &
dom (f2 * p) c= dom p )
by RELAT_1:44, RELAT_1:46;
thus (f1 +* f2) * p =
(f2 +* f1) * p
by A1, FUNCT_4:35
.=
(f2 * p) +* (f1 * p)
by FUNCT_7:11
.=
f1 * p
by A23, FUNCT_4:20
.=
the
Arity of
E . (g1 . o)
by A5, A21, A22
.=
the
Arity of
E . ((g1 +* g2) . o)
by A6, A20, FUNCT_4:12
;
:: thesis: verum end;