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