now :: thesis: for y being object holds (ProjMap1 (F,x)) . y < +infty

let y be object ; :: thesis: (ProjMap1 (F,x)) . b₁ < +infty

per cases ( not y in dom (ProjMap1 (F,x)) or y in dom (ProjMap1 (F,x)) ) ;

suppose not y in dom (ProjMap1 (F,x)) ; :: thesis: (ProjMap1 (F,x)) . b₁ < +infty

hence (ProjMap1 (F,x)) . y < +infty by FUNCT_1:def 2; :: thesis: verum

end;

suppose y in dom (ProjMap1 (F,x)) ; :: thesis: (ProjMap1 (F,x)) . b₁ < +infty

then reconsider y1 = y as Element of Y ;
(ProjMap1 (F,x)) . y = F . (x,y1) by MESFUNC9:def 6;
hence (ProjMap1 (F,x)) . y < +infty by MESFUNC5:def 6; :: thesis: verum

end;

end;

end;

hence ProjMap1 (F,x) is without+infty by MESFUNC5:def 6; :: thesis: verum