let F be Function; :: thesis: ( F is empty implies ( F is uncurrying & F is currying & F is commuting ) )
assume A1: F is empty ; :: thesis: ( F is uncurrying & F is currying & F is commuting )
hence for x being set st x in dom F holds
x is Function-yielding Function ; :: according to WAYBEL27:def 1 :: thesis: ( ( for f being Function st f in dom F holds
F . f = uncurry f ) & F is currying & F is commuting )
thus for f being Function st f in dom F holds
F . f = uncurry f by A1; :: thesis: ( F is currying & F is commuting )
thus for x being set st x in dom F holds
( x is Function & proj1 x is Relation ) by A1; :: according to WAYBEL27:def 2 :: thesis: ( ( for f being Function st f in dom F holds
F . f = curry f ) & F is commuting )
thus for f being Function st f in dom F holds
F . f = curry f by A1; :: thesis: F is commuting
thus for x being set st x in dom F holds
x is Function-yielding Function by A1; :: according to WAYBEL27:def 3 :: thesis: for f being Function st f in dom F holds
F . f = commute f
thus for f being Function st f in dom F holds
F . f = commute f by A1; :: thesis: verum