set H = G ** F;
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom (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 Def19;
hence (G ** F) . x is set ; :: thesis: verum