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))
A2: the ResultSort of S1 tolerates the ResultSort of S2 by A1;
A3: rng the Arity of S2 c= the carrier of S2 * ;
A4: rng the ResultSort of S2 c= the carrier of S2 ;
A5: rng the ResultSort of S1 c= the carrier of S1 ;
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 A6: 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 H₁( non void Signature) -> ManySortedSet of the carrier of $1 = the carrier of $1 -indexing f;
deffunc H₂( non void Signature) -> non empty non void strict ManySortedSign = $1 with-replacement (f,g);
A7: dom H₁(S2) = the carrier of S2 by PARTFUN1:def 2;
A8: H₁(S1) tolerates H₁(S2) by Th19;
A9: S1 +* S2 is Extension of S1 by A1, Th47;
then reconsider F1 = H₁(S1) as Function of the carrier of S1, the carrier of H₂(S1) by A6, Th36, Th52;
A10: dom (H₁(S1) * the ResultSort of S1) = the carrier' of S1 by PARTFUN1:def 2;
deffunc H₃( non void Signature) -> ManySortedSet of the carrier' of $1 = the carrier' of $1 -indexing g;
A11: dom H₁(S1) = the carrier of S1 by PARTFUN1:def 2;
A12: dom H₃(S1) = the carrier' of S1 by PARTFUN1:def 2;
set g1 = the rng-retract of H₃(S1);
set g2 = the rng-retract of H₃(S2);
A13: the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by CIRCCOMB:def 2;
A14: rng the rng-retract of H₃(S2) c= dom H₃(S2) by Th23;
A15: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by CIRCCOMB:def 2;
then H₃(S1 +* S2) = H₃(S1) \/ H₃(S2) by Th20;
then A16: rng H₃(S1 +* S2) = (rng H₃(S1)) \/ (rng H₃(S2)) by RELAT_1:12;
A17: dom H₃(S2) = the carrier' of S2 by PARTFUN1:def 2;
A18: S1 +* S2 is Extension of S2 by Th48;
then reconsider F2 = H₁(S2) as Function of the carrier of S2, the carrier of H₂(S2) by A6, Th36, Th52;
A19: dom (H₁(S2) * the ResultSort of S2) = the carrier' of S2 by PARTFUN1:def 2;
A20: the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by CIRCCOMB:def 2;
then A21: H₁(S1 +* S2) = H₁(S1) +* H₁(S2) by Th18;
H₁(S1 +* S2) = H₁(S1) \/ H₁(S2) by A20, Th20;
then A22: rng H₁(S1 +* S2) = (rng H₁(S1)) \/ (rng H₁(S2)) by RELAT_1:12;
A23: dom ((F2 *) * the Arity of S2) = the carrier' of S2 by FUNCT_2:def 1;
A24: dom (F2 *) = the carrier of S2 * by FUNCT_2:def 1;
H₃(S1 +* S2) = H₃(S1) +* H₃(S2) by A15, Th18;
then reconsider gg = the rng-retract of H₃(S1) +* the rng-retract of H₃(S2) as rng-retract of H₃(S1 +* S2) by Th19, Th27;
A25: rng the rng-retract of H₃(S1) c= dom H₃(S1) by Th23;
A26: the ResultSort of H₂(S1 +* S2) = (H₁(S1 +* S2) * the ResultSort of (S1 +* S2)) * gg by A6, Th38
.= ((H₁(S1) * the ResultSort of S1) +* (H₁(S2) * the ResultSort of S2)) * gg by A13, A21, A5, A4, A11, A7, Th19, FUNCT_4:69
.= ((H₁(S1) * the ResultSort of S1) * the rng-retract of H₃(S1)) +* ((H₁(S2) * the ResultSort of S2) * the rng-retract of H₃(S2)) by A8, A25, A14, A12, A17, A10, A19, A2, Th4, FUNCT_4:69
.= the ResultSort of H₂(S1) +* ((H₁(S2) * the ResultSort of S2) * the rng-retract of H₃(S2)) by A6, A9, Th38, Th52
.= the ResultSort of H₂(S1) +* the ResultSort of H₂(S2) by A6, A18, Th38, Th52 ;
A27: the carrier of H₂(S1 +* S2) = rng H₁(S1 +* S2) by A6, Def4;
A28: dom ((F1 *) * the Arity of S1) = the carrier' of S1 by FUNCT_2:def 1;
reconsider FS = H₁(S1 +* S2) as Function of the carrier of (S1 +* S2), the carrier of H₂(S1 +* S2) by A6, Th36;
A29: (rng the Arity of (S1 +* S2)) /\ (dom (FS *)) c= rng the Arity of (S1 +* S2) by XBOOLE_1:17;
A30: the Arity of (S1 +* S2) = the Arity of S1 +* the Arity of S2 by CIRCCOMB:def 2;
A31: f,g form_a_replacement_in S1 by A6, A9, Th52;
then A32: the carrier of H₂(S1) = rng H₁(S1) by Def4;
A33: the carrier' of H₂(S1) = rng H₃(S1) by A31, Def4;
A34: the carrier' of H₂(S1 +* S2) = rng H₃(S1 +* S2) by A6, Def4;
A35: dom (F1 *) = the carrier of S1 * by FUNCT_2:def 1;
the Arity of S1 tolerates the Arity of S2 by A1;
then the Arity of (S1 +* S2) = the Arity of S1 \/ the Arity of S2 by A30, FUNCT_4:30;
then rng the Arity of (S1 +* S2) = (rng the Arity of S1) \/ (rng the Arity of S2) by RELAT_1:12;
then rng the Arity of (S1 +* S2) c= ( the carrier of S1 *) \/ ( the carrier of S2 *) by XBOOLE_1:13;
then rng the Arity of (S1 +* S2) c= dom ((F1 *) +* (F2 *)) by A35, A24, FUNCT_4:def 1;
then A36: (rng the Arity of (S1 +* S2)) /\ (dom (FS *)) c= dom ((F1 *) +* (F2 *)) by A29;
A37: f,g form_a_replacement_in S2 by A6, A18, Th52;
then A38: the carrier of H₂(S2) = rng H₁(S2) by Def4;
A39: the carrier' of H₂(S2) = rng H₃(S2) by A37, Def4;
A40: F1 * tolerates F2 * by Th6, Th19;
A41: (F1 *) +* (F2 *) c= (F1 *) \/ (F2 *) by FUNCT_4:29;
F2 = FS | the carrier of S2 by A20, Th17, XBOOLE_1:7;
then A42: F2 * c= FS * by Th5, RELAT_1:59;
F1 = FS | the carrier of S1 by A20, Th17, XBOOLE_1:7;
then F1 * c= FS * by Th5, RELAT_1:59;
then (F1 *) \/ (F2 *) c= FS * by A42, XBOOLE_1:8;
then A43: (F1 *) +* (F2 *) c= FS * by A41;
A44: the Arity of S1 tolerates the Arity of S2 by A1;
A45: rng the Arity of S1 c= the carrier of S1 * ;
A46: f,g form_a_replacement_in S1 by A6, A9, Th52;
the Arity of H₂(S1 +* S2) = ((FS *) * the Arity of (S1 +* S2)) * gg by A6, Th37
.= (((F1 *) +* (F2 *)) * the Arity of (S1 +* S2)) * gg by A43, A36, Th2
.= (((F1 *) * the Arity of S1) +* ((F2 *) * the Arity of S2)) * gg by A30, A8, A45, A3, A35, A24, Th6, FUNCT_4:69
.= (((F1 *) * the Arity of S1) * the rng-retract of H₃(S1)) +* (((F2 *) * the Arity of S2) * the rng-retract of H₃(S2)) by A25, A14, A12, A17, A40, A44, A28, A23, Th4, FUNCT_4:69
.= the Arity of H₂(S1) +* (((F2 *) * the Arity of S2) * the rng-retract of H₃(S2)) by A46, Th37
.= the Arity of H₂(S1) +* the Arity of H₂(S2) by A6, A18, Th37, Th52 ;
hence (S1 +* S2) with-replacement (f,g) = (S1 with-replacement (f,g)) +* (S2 with-replacement (f,g)) by A22, A27, A32, A38, A16, A34, A33, A39, A26, CIRCCOMB:def 2; :: thesis: verum