let X be set ; :: thesis: compose ({},X) = id X
ex f being ManySortedFunction of NAT st
( compose ({},X) = f . 0 & f . 0 = id X & ( for i being 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 Def3, CARD_1:27;
hence compose ({},X) = id X ; :: thesis: verum