set h = f => g;

let x be Element of Funcs (A,B); :: according to PARTIT_2:def 3 :: thesis: (f => g) . ((f => g) . x) = x

A1: ( (f ") * (f ") = id A & g * g = id B ) by Th9;

thus (f => g) . ((f => g) . x) = (f => g) . ((g * x) * (f ")) by HILBERT3:def 1

.= (g * ((g * x) * (f "))) * (f ") by HILBERT3:def 1

.= ((g * (g * x)) * (f ")) * (f ") by RELAT_1:36

.= (((g * g) * x) * (f ")) * (f ") by RELAT_1:36

.= x * (id A) by A1, RELAT_1:36

.= x ; :: thesis: verum

let x be Element of Funcs (A,B); :: according to PARTIT_2:def 3 :: thesis: (f => g) . ((f => g) . x) = x

A1: ( (f ") * (f ") = id A & g * g = id B ) by Th9;

thus (f => g) . ((f => g) . x) = (f => g) . ((g * x) * (f ")) by HILBERT3:def 1

.= (g * ((g * x) * (f "))) * (f ") by HILBERT3:def 1

.= ((g * (g * x)) * (f ")) * (f ") by RELAT_1:36

.= (((g * g) * x) * (f ")) * (f ") by RELAT_1:36

.= x * (id A) by A1, RELAT_1:36

.= x ; :: thesis: verum