let S1, S2, E be non empty Signature; ( 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 )
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
;
INSTALG1:def 2,
ALGSPEC1:def 5 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;
INSTALG1:def 2,
ALGSPEC1:def 5 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; ( S1 tolerates S2 & E is Extension of S1 +* S2 implies ( E is Extension of S1 & E is Extension of S2 ) )
assume
S1 tolerates S2
; ( 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; verum