let A be non empty set ; :: thesis: for S being CatSignature of A
for s being SortSymbol of S ex a, b being Element of A st s = homsym a,b
let S be CatSignature of A; :: thesis: for s being SortSymbol of S ex a, b being Element of A st s = homsym a,b
let s be SortSymbol of S; :: thesis: ex a, b being Element of A st s = homsym a,b
the carrier of S = [:{0 },(2 -tuples_on A):] by Def7;
then A1: ( s = [(s `1 ),(s `2 )] & s `1 in {0 } & s `2 in 2 -tuples_on A ) by MCART_1:10, MCART_1:23;
then s `2 in { z where z is Element of A * : len z = 2 } by FINSEQ_2:def 4;
then consider z being Element of A * such that
A2: ( s `2 = z & len z = 2 ) ;
A3: z = <*(z . 1),(z . 2)*> by A2, FINSEQ_1:61;
then ( z . 1 in {(z . 1),(z . 2)} & z . 2 in {(z . 1),(z . 2)} & rng z = {(z . 1),(z . 2)} & rng z c= A ) by FINSEQ_2:147, TARSKI:def 2;
then reconsider a = z . 1, b = z . 2 as Element of A ;
take a ; :: thesis: ex b being Element of A st s = homsym a,b
take b ; :: thesis: s = homsym a,b
thus s = homsym a,b by A1, A2, A3, TARSKI:def 1; :: thesis: verum