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

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

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: -infty < (ProjMap2 (F,y)) . b₁

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

end;

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

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

end;

end;

end;

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