let S1, S2 be non empty Signature; :: thesis: ( S1 tolerates S2 implies S1 +* S2 is Extension of S1 )
assume that
A1: the Arity of S1 tolerates the Arity of S2 and
A2: the ResultSort of S1 tolerates the ResultSort of S2 ; :: according to CIRCCOMB:def 1 :: thesis: S1 +* S2 is Extension of S1
set S = S1 +* S2;
set f1 = id the carrier of S1;
set g1 = id the carrier' of S1;
thus ( dom (id the carrier of S1) = the carrier of S1 & dom (id the carrier' of S1) = the carrier' of S1 ) by RELAT_1:71; :: according to PUA2MSS1:def 13,INSTALG1:def 2,ALGSPEC1:def 5 :: thesis: ( rng (id the carrier of S1) c= the carrier of (S1 +* S2) & rng (id the carrier' of S1) c= the carrier' of (S1 +* S2) & the ResultSort of S1 * (id the carrier of S1) = (id the carrier' of S1) * the ResultSort of (S1 +* S2) & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S1 or not b₂ = the Arity of S1 . b₁ or b₂ * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . b₁) ) ) )
A3: ( rng (id the carrier of S1) = the carrier of S1 & rng (id the carrier' of S1) = the carrier' of S1 ) by RELAT_1:71;
( the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 & the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 ) by CIRCCOMB:def 2;
hence ( rng (id the carrier of S1) c= the carrier of (S1 +* S2) & rng (id the carrier' of S1) c= the carrier' of (S1 +* S2) ) by A3, XBOOLE_1:7; :: thesis: ( the ResultSort of S1 * (id the carrier of S1) = (id the carrier' of S1) * the ResultSort of (S1 +* S2) & ( for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S1 or not b₂ = the Arity of S1 . b₁ or b₂ * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . b₁) ) ) )
A4: ( dom the ResultSort of S1 = the carrier' of S1 & rng the ResultSort of S1 c= the carrier of S1 ) by FUNCT_2:def 1;
the ResultSort of (S1 +* S2) = the ResultSort of S1 +* the ResultSort of S2 by CIRCCOMB:def 2;
then the ResultSort of S1 c= the ResultSort of (S1 +* S2) by A2, FUNCT_4:29;
then the ResultSort of S1 = the ResultSort of (S1 +* S2) | the carrier' of S1 by A4, GRFUNC_1:64;
then the ResultSort of S1 = the ResultSort of (S1 +* S2) * (id the carrier' of S1) by RELAT_1:94;
hence (id the carrier of S1) * the ResultSort of S1 = the ResultSort of (S1 +* S2) * (id the carrier' of S1) by A4, RELAT_1:79; :: thesis: for b₁ being set
for b₂ being set holds
( not b₁ in the carrier' of S1 or not b₂ = the Arity of S1 . b₁ or b₂ * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . b₁) )
let o be set ; :: thesis: for b₁ being set holds
( not o in the carrier' of S1 or not b₁ = the Arity of S1 . o or b₁ * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . o) )
let p be Function; :: thesis: ( not o in the carrier' of S1 or not p = the Arity of S1 . o or p * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . o) )
assume A5: ( o in the carrier' of S1 & p = the Arity of S1 . o ) ; :: thesis: p * (id the carrier of S1) = the Arity of (S1 +* S2) . ((id the carrier' of S1) . o)
A6: ( dom the Arity of S1 = the carrier' of S1 & rng the Arity of S1 c= the carrier of S1 * ) by FUNCT_2:def 1;
then p in rng the Arity of S1 by A5, FUNCT_1:def 5;
then p is FinSequence of the carrier of S1 by FINSEQ_1:def 11;
then rng p c= the carrier of S1 by FINSEQ_1:def 4;
hence (id the carrier of S1) * p = p by RELAT_1:79
.= (the Arity of S1 +* the Arity of S2) . o by A1, A5, A6, FUNCT_4:16
.= the Arity of (S1 +* S2) . o by CIRCCOMB:def 2
.= the Arity of (S1 +* S2) . ((id the carrier' of S1) . o) by A5, FUNCT_1:35 ;
:: thesis: verum