let S1, S2 be non void Signature; :: thesis: ( S1 tolerates S2 implies for f, g being Function st f,g form_a_replacement_in S1 +* S2 holds
(S1 +* S2) with-replacement f,g = (S1 with-replacement f,g) +* (S2 with-replacement f,g) )
assume A1:
S1 tolerates S2
; :: thesis: for f, g being Function st f,g form_a_replacement_in S1 +* S2 holds
(S1 +* S2) with-replacement f,g = (S1 with-replacement f,g) +* (S2 with-replacement f,g)
set S = S1 +* S2;
let f, g be Function; :: thesis: ( f,g form_a_replacement_in S1 +* S2 implies (S1 +* S2) with-replacement f,g = (S1 with-replacement f,g) +* (S2 with-replacement f,g) )
assume A2:
f,g form_a_replacement_in S1 +* S2
; :: thesis: (S1 +* S2) with-replacement f,g = (S1 with-replacement f,g) +* (S2 with-replacement f,g)
deffunc H1( non void Signature) -> non empty non void strict ManySortedSign = $1 with-replacement f,g;
deffunc H2( non void Signature) -> ManySortedSet of = the carrier of $1 -indexing f;
deffunc H3( non void Signature) -> ManySortedSet of = the carrier' of $1 -indexing g;
A3:
( S1 +* S2 is Extension of S1 & S1 +* S2 is Extension of S2 )
by A1, Th49, Th50;
then A4:
( f,g form_a_replacement_in S1 & f,g form_a_replacement_in S2 )
by A2, Th54;
A5:
( the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 & the carrier of (H1(S1) +* H1(S2)) = the carrier of H1(S1) \/ the carrier of H1(S2) )
by CIRCCOMB:def 2;
then
H2(S1 +* S2) = H2(S1) \/ H2(S2)
by Th21;
then A6:
rng H2(S1 +* S2) = (rng H2(S1)) \/ (rng H2(S2))
by RELAT_1:26;
A7:
( the carrier of H1(S1 +* S2) = rng H2(S1 +* S2) & the carrier of H1(S1) = rng H2(S1) & the carrier of H1(S2) = rng H2(S2) )
by A2, A4, Def4;
A8:
( the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 & the carrier' of (H1(S1) +* H1(S2)) = the carrier' of H1(S1) \/ the carrier' of H1(S2) )
by CIRCCOMB:def 2;
then
H3(S1 +* S2) = H3(S1) \/ H3(S2)
by Th21;
then A9:
rng H3(S1 +* S2) = (rng H3(S1)) \/ (rng H3(S2))
by RELAT_1:26;
A10:
( the carrier' of H1(S1 +* S2) = rng H3(S1 +* S2) & the carrier' of H1(S1) = rng H3(S1) & the carrier' of H1(S2) = rng H3(S2) )
by A2, A4, Def4;
A11:
( the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 & the Arity of (H1(S1) +* H1(S2)) = the Arity of H1(S1) +* the Arity of H1(S2) )
by CIRCCOMB:def 2;
A12:
( the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 & the ResultSort of (H1(S1) +* H1(S2)) = the ResultSort of H1(S1) +* the ResultSort of H1(S2) )
by CIRCCOMB:def 2;
consider g1 being rng-retract of H3(S1), g2 being rng-retract of H3(S2);
( H3(S1) tolerates H3(S2) & H3(S1 +* S2) = H3(S1) +* H3(S2) )
by A8, Th19, Th20;
then reconsider gg = g1 +* g2 as rng-retract of H3(S1 +* S2) by Th28;
A13:
( H2(S1 +* S2) = H2(S1) +* H2(S2) & H2(S1) tolerates H2(S2) )
by A5, Th19, Th20;
A14:
( rng the ResultSort of S1 c= the carrier of S1 & rng the ResultSort of S2 c= the carrier of S2 )
;
A15:
( dom H2(S1) = the carrier of S1 & dom H2(S2) = the carrier of S2 )
by PARTFUN1:def 4;
A16:
( rng g1 c= dom H3(S1) & rng g2 c= dom H3(S2) )
by Th24;
A17:
( dom H3(S1) = the carrier' of S1 & dom H3(S2) = the carrier' of S2 )
by PARTFUN1:def 4;
A18:
( dom (H2(S1) * the ResultSort of S1) = the carrier' of S1 & dom (H2(S2) * the ResultSort of S2) = the carrier' of S2 )
by PARTFUN1:def 4;
A19:
the ResultSort of S1 tolerates the ResultSort of S2
by A1, CIRCCOMB:def 1;
A20: the ResultSort of H1(S1 +* S2) =
(H2(S1 +* S2) * the ResultSort of (S1 +* S2)) * gg
by A2, Th39
.=
((H2(S1) * the ResultSort of S1) +* (H2(S2) * the ResultSort of S2)) * gg
by A12, A13, A14, A15, FUNCT_4:73
.=
((H2(S1) * the ResultSort of S1) * g1) +* ((H2(S2) * the ResultSort of S2) * g2)
by A13, A16, A17, A18, A19, Th4, FUNCT_4:73
.=
the ResultSort of H1(S1) +* ((H2(S2) * the ResultSort of S2) * g2)
by A2, A3, Th39, Th54
.=
the ResultSort of H1(S1) +* the ResultSort of H1(S2)
by A2, A3, Th39, Th54
;
reconsider FS = H2(S1 +* S2) as Function of the carrier of (S1 +* S2),the carrier of H1(S1 +* S2) by A2, Th37;
reconsider F1 = H2(S1) as Function of the carrier of S1,the carrier of H1(S1) by A2, A3, Th37, Th54;
reconsider F2 = H2(S2) as Function of the carrier of S2,the carrier of H1(S2) by A2, A3, Th37, Th54;
the Arity of S1 tolerates the Arity of S2
by A1, CIRCCOMB:def 1;
then
the Arity of (S1 +* S2) = the Arity of S1 \/ the Arity of S2
by A11, FUNCT_4:31;
then A21:
rng the Arity of (S1 +* S2) = (rng the Arity of S1) \/ (rng the Arity of S2)
by RELAT_1:26;
A22:
( rng the Arity of S1 c= the carrier of S1 * & rng the Arity of S2 c= the carrier of S2 * )
;
A23:
rng the Arity of (S1 +* S2) c= (the carrier of S1 * ) \/ (the carrier of S2 * )
by A21, XBOOLE_1:13;
( F1 = FS | the carrier of S1 & F2 = FS | the carrier of S2 )
by A5, Th18, XBOOLE_1:7;
then
( F1 * c= FS * & F2 * c= FS * )
by Th5, RELAT_1:88;
then
( (F1 * ) \/ (F2 * ) c= FS * & (F1 * ) +* (F2 * ) c= (F1 * ) \/ (F2 * ) )
by FUNCT_4:30, XBOOLE_1:8;
then A24:
(F1 * ) +* (F2 * ) c= FS *
by XBOOLE_1:1;
A25:
( dom (F1 * ) = the carrier of S1 * & dom (F2 * ) = the carrier of S2 * )
by FUNCT_2:def 1;
then
( rng the Arity of (S1 +* S2) c= dom ((F1 * ) +* (F2 * )) & (rng the Arity of (S1 +* S2)) /\ (dom (FS * )) c= rng the Arity of (S1 +* S2) )
by A23, FUNCT_4:def 1, XBOOLE_1:17;
then A26:
(rng the Arity of (S1 +* S2)) /\ (dom (FS * )) c= dom ((F1 * ) +* (F2 * ))
by XBOOLE_1:1;
A27:
F1 * tolerates F2 *
by Th20, Th6;
A28:
the Arity of S1 tolerates the Arity of S2
by A1, CIRCCOMB:def 1;
A29:
( dom ((F1 * ) * the Arity of S1) = the carrier' of S1 & dom ((F2 * ) * the Arity of S2) = the carrier' of S2 )
by FUNCT_2:def 1;
the Arity of H1(S1 +* S2) =
((FS * ) * the Arity of (S1 +* S2)) * gg
by A2, Th38
.=
(((F1 * ) +* (F2 * )) * the Arity of (S1 +* S2)) * gg
by A24, A26, Th2
.=
(((F1 * ) * the Arity of S1) +* ((F2 * ) * the Arity of S2)) * gg
by A11, A13, A22, A25, Th6, FUNCT_4:73
.=
(((F1 * ) * the Arity of S1) * g1) +* (((F2 * ) * the Arity of S2) * g2)
by A16, A17, A27, A28, A29, Th4, FUNCT_4:73
.=
the Arity of H1(S1) +* (((F2 * ) * the Arity of S2) * g2)
by A2, A3, Th38, Th54
.=
the Arity of H1(S1) +* the Arity of H1(S2)
by A2, A3, Th38, Th54
;
hence
(S1 +* S2) with-replacement f,g = (S1 with-replacement f,g) +* (S2 with-replacement f,g)
by A6, A7, A9, A10, A20, CIRCCOMB:def 2; :: thesis: verum