let C1, C2 be strict ManySortedSign ; :: thesis: ( C1 is empty & C1 is void & C2 is empty & C2 is void implies C1 = C2 )
assume that
A1:
( C1 is empty & C1 is void )
and
A2:
( C2 is empty & C2 is void )
; :: thesis: C1 = C2
C1 = C2
proof
A3:
( the
carrier of
C1 = {} & the
carrier of
C2 = {} )
by A1, A2;
A4:
( the
carrier' of
C1 = {} & the
carrier' of
C2 = {} )
by A1, A2;
then reconsider RS = the
ResultSort of
C1,
RT = the
ResultSort of
C2 as
Function of
{} ,
{} by A3;
A5:
(
RS in {(id {} )} &
RT in {(id {} )} )
by ALTCAT_1:3, FUNCT_2:12;
reconsider A = the
Arity of
C1,
B = the
Arity of
C2 as
Function of
{} ,
{{} } by A3, A4, FUNCT_7:19;
A6:
A = B
by FUNCT_2:66;
the
ResultSort of
C1 =
id {}
by A5, TARSKI:def 1
.=
the
ResultSort of
C2
by A5, TARSKI:def 1
;
hence
C1 = C2
by A3, A4, A6;
:: thesis: verum
end;
hence
C1 = C2
; :: thesis: verum