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

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

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

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

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

end;

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

then reconsider x1 = x as Element of X ;
(ProjMap2 (F,y)) . x = F . (x1,y) by MESFUNC9:def 7;
hence (ProjMap2 (F,y)) . x < +infty by MESFUNC5:def 6; :: thesis: verum

end;

end;

end;

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