let X be set ; :: thesis: compose {} ,X = id X
ex f being ManySortedFunction of st
( compose {} ,X = f . 0 & f . 0 = id X & ( for i being Element of NAT st i + 1 in dom {} holds
for g, h being Function st g = f . i & h = {} . (i + 1) holds
f . (i + 1) = h * g ) ) by Def4, CARD_1:47;
hence compose {} ,X = id X ; :: thesis: verum