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
A1: the carrier of S = [:{0 },(2 -tuples_on A):] by Def7;
then s `2 in 2 -tuples_on A by MCART_1:10;
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 and
A3: len z = 2 ;
A4: ( z . 1 in {(z . 1),(z . 2)} & z . 2 in {(z . 1),(z . 2)} ) by TARSKI:def 2;
A5: z = <*(z . 1),(z . 2)*> by A3, FINSEQ_1:61;
then rng z = {(z . 1),(z . 2)} by FINSEQ_2:147;
then reconsider a = z . 1, b = z . 2 as Element of A by A4;
take a ; :: thesis: ex b being Element of A st s = homsym a,b
take b ; :: thesis: s = homsym a,b
( s = [(s `1 ),(s `2 )] & s `1 in {0 } ) by A1, MCART_1:10, MCART_1:23;
hence s = homsym a,b by A2, A5, TARSKI:def 1; :: thesis: verum