let A1, A2 be set ; :: thesis: for S being CatSignature of A1 st S is CatSignature of A2 holds
A1 = A2
let S be CatSignature of A1; :: thesis: ( S is CatSignature of A2 implies A1 = A2 )
assume that
CatSign A2 is Subsignature of S and
A1: the carrier of S = [:{0},(2 -tuples_on A2):] ; :: according to CATALG_1:def 5 :: thesis: A1 = A2
A2: [:{0},(2 -tuples_on A1):] = [:{0},(2 -tuples_on A2):] by A1, Def5;
then A3: 2 -tuples_on A1 c= 2 -tuples_on A2 by ZFMISC_1:94;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: A2 c= A1

let x be object ; :: thesis: ( x in A1 implies x in A2 )
assume x in A1 ; :: thesis: x in A2
then <*x,x*> in 2 -tuples_on A1 by FINSEQ_2:137;
then <*x,x*> in 2 -tuples_on A2 by A3;
hence x in A2 by FINSEQ_2:138; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A2 or x in A1 )
assume x in A2 ; :: thesis: x in A1
then A4: <*x,x*> in 2 -tuples_on A2 by FINSEQ_2:137;
2 -tuples_on A2 c= 2 -tuples_on A1 by A2, ZFMISC_1:94;
hence x in A1 by A4, FINSEQ_2:138; :: thesis: verum