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 A2: ( S1 is Subsignature of E & S2 is Subsignature of E ) ; :: according to ALGSPEC1:def 5 :: thesis: S1 tolerates S2
then ( the Arity of S1 c= the Arity of E & the Arity of S2 c= the Arity of E ) by INSTALG1:12;
hence the Arity of S1 tolerates the Arity of S2 by PARTFUN1:131; :: according to CIRCCOMB:def 1 :: thesis: the ResultSort of S1 tolerates the ResultSort of S2
( the ResultSort of S1 c= the ResultSort of E & the ResultSort of S2 c= the ResultSort of E ) by A2, INSTALG1:12;
hence the ResultSort of S1 tolerates the ResultSort of S2 by PARTFUN1:131; :: thesis: verum

end;

( the carrier of S1 c= the carrier of S1 \/ the carrier of S2 & the carrier of S2 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) & id the carrier of S2 c= id (the carrier of S1 \/ the carrier of S2) ) by FUNCT_4:4;
then A3: id the carrier of S1 tolerates id the carrier of S2 by PARTFUN1:131;
A4: ( 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;
( E is Extension of S1 & E is Extension of S2 implies E is Extension of S1 +* S2 )

proof

assume ( id the carrier of S1, id the carrier' of S1 form_morphism_between S1,E & 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
then (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 A3, Th51;
then id the carrier of (S1 +* S2),(id the carrier' of S1) +* (id the carrier' of S2) form_morphism_between S1 +* S2,E by A4, FUNCT_4:23;
hence id the carrier of (S1 +* S2), id the carrier' of (S1 +* S2) form_morphism_between S1 +* S2,E by A4, FUNCT_4:23; :: 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 ( S1 +* S2 is Extension of S1 & S1 +* S2 is Extension of S2 ) by Th49, Th50;
hence ( not E is Extension of S1 +* S2 or ( E is Extension of S1 & E is Extension of S2 ) ) by Th48; :: thesis: verum