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 Def5;
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:44;
then rng z = {(z . 1),(z . 2)} by FINSEQ_2:127;
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:21;
hence s = homsym (a,b) by A2, A5, TARSKI:def 1; :: thesis: verum