let X be set ; :: thesis: for F being non empty SubStr of GPFuncs X st id X is Element of F holds
( F is unital & the_unity_wrt the multF of F = id X )
let F be non empty SubStr of GPFuncs X; :: thesis: ( id X is Element of F implies ( F is unital & the_unity_wrt the multF of F = id X ) )
the_unity_wrt H₂( GPFuncs X) = id X by Th69;
hence ( id X is Element of F implies ( F is unital & the_unity_wrt the multF of F = id X ) ) by Th30; :: thesis: verum