A1:
( not C is empty implies ex F being Function of (Ob C),(Mor C) st
for o being Element of Ob C holds F . o = id- o )
A4:
( C is empty implies ex F being Function of (Ob C),(Mor C) st F = {} )
A5:
for F1, F2 being Function of (Ob C),(Mor C) st ( for o being Element of Ob C holds F1 . o = id- o ) & ( for o being Element of Ob C holds F2 . o = id- o ) holds
F1 = F2
thus
( ( for b1 being Function of (Ob C),(Mor C) holds verum ) & ( not C is empty implies ex b1 being Function of (Ob C),(Mor C) st
for o being Element of Ob C holds b1 . o = id- o ) & ( C is empty implies ex b1 being Function of (Ob C),(Mor C) st b1 = {} ) & ( for b1, b2 being Function of (Ob C),(Mor C) holds
( ( not C is empty & ( for o being Element of Ob C holds b1 . o = id- o ) & ( for o being Element of Ob C holds b2 . o = id- o ) implies b1 = b2 ) & ( C is empty & b1 = {} & b2 = {} implies b1 = b2 ) ) ) )
by A1, A4, A5; verum