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