set H = G ** F;
let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 (G ** F) or (G ** F) . x is set )
reconsider f = F . x as Function ;
reconsider g = G . x as Function ;
assume x in dom (G ** F) ; :: thesis: (G ** F) . x is set
then (G ** F) . x = g * f by Def24;
hence (G ** F) . x is set ; :: thesis: verum