let S1, S2, E be non empty Signature; :: thesis: ( E is Extension of S1 & E is Extension of S2 iff ( S1 tolerates S2 & E is Extension of S1 +* S2 ) )
set f1 = id the carrier of S1;
set g1 = id the carrier' of S1;
set f2 = id the carrier of S2;
set g2 = id the carrier' of S2;
A1: ( E is Extension of S1 & E is Extension of S2 implies S1 tolerates S2 )
proof
assume that
A2: S1 is Subsignature of E and
A3: S2 is Subsignature of E ; :: according to ALGSPEC1:def 5 :: thesis: S1 tolerates S2
A4: the Arity of S2 c= the Arity of E by A3, INSTALG1:11;
the Arity of S1 c= the Arity of E by A2, INSTALG1:11;
hence the Arity of S1 tolerates the Arity of S2 by A4, PARTFUN1:52; :: according to CIRCCOMB:def 1 :: thesis: the ResultSort of S1 tolerates the ResultSort of S2
A5: the ResultSort of S2 c= the ResultSort of E by A3, INSTALG1:11;
the ResultSort of S1 c= the ResultSort of E by A2, INSTALG1:11;
hence the ResultSort of S1 tolerates the ResultSort of S2 by A5, PARTFUN1:52; :: thesis: verum
end;
A6: the carrier of (S1 +* S2) = the carrier of S1 \/ the carrier of S2 by CIRCCOMB:def 2;
the carrier of S2 c= the carrier of S1 \/ the carrier of S2 by XBOOLE_1:7;
then A7: id the carrier of S2 c= id ( the carrier of S1 \/ the carrier of S2) by FUNCT_4:3;
A8: the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by CIRCCOMB:def 2;
the carrier of S1 c= the carrier of S1 \/ the carrier of S2 by XBOOLE_1:7;
then id the carrier of S1 c= id ( the carrier of S1 \/ the carrier of S2) by FUNCT_4:3;
then A9: id the carrier of S1 tolerates id the carrier of S2 by A7, PARTFUN1:52;
( E is Extension of S1 & E is Extension of S2 implies E is Extension of S1 +* S2 )
proof
assume that
A10: id the carrier of S1, id the carrier' of S1 form_morphism_between S1,E and
A11: id the carrier of S2, id the carrier' of S2 form_morphism_between S2,E ; :: according to INSTALG1:def 2,ALGSPEC1:def 5 :: thesis: E is Extension of S1 +* S2
(id the carrier of S1) +* (id the carrier of S2),(id the carrier' of S1) +* (id the carrier' of S2) form_morphism_between S1 +* S2,E by A9, A10, A11, Th49;
then id the carrier of (S1 +* S2),(id the carrier' of S1) +* (id the carrier' of S2) form_morphism_between S1 +* S2,E by A6, FUNCT_4:22;
hence id the carrier of (S1 +* S2), id the carrier' of (S1 +* S2) form_morphism_between S1 +* S2,E by A8, FUNCT_4:22; :: according to INSTALG1:def 2,ALGSPEC1:def 5 :: thesis: verum
end;
hence ( E is Extension of S1 & E is Extension of S2 implies ( S1 tolerates S2 & E is Extension of S1 +* S2 ) ) by A1; :: thesis: ( S1 tolerates S2 & E is Extension of S1 +* S2 implies ( E is Extension of S1 & E is Extension of S2 ) )
assume S1 tolerates S2 ; :: thesis: ( not E is Extension of S1 +* S2 or ( E is Extension of S1 & E is Extension of S2 ) )
then A12: S1 +* S2 is Extension of S1 by Th47;
S1 +* S2 is Extension of S2 by Th48;
hence ( not E is Extension of S1 +* S2 or ( E is Extension of S1 & E is Extension of S2 ) ) by A12, Th46; :: thesis: verum