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

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

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

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

end;

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

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

end;

end;

end;

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