let X1, X2 be non empty set ; :: thesis: for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is nonnegative holds
( ProjPMap1 (f,x) is nonnegative & ProjPMap2 (f,y) is nonnegative )
let x be Element of X1; :: thesis: for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is nonnegative holds
( ProjPMap1 (f,x) is nonnegative & ProjPMap2 (f,y) is nonnegative )
let y be Element of X2; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL st f is nonnegative holds
( ProjPMap1 (f,x) is nonnegative & ProjPMap2 (f,y) is nonnegative )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( f is nonnegative implies ( ProjPMap1 (f,x) is nonnegative & ProjPMap2 (f,y) is nonnegative ) )
assume A1: f is nonnegative ; :: thesis: ( ProjPMap1 (f,x) is nonnegative & ProjPMap2 (f,y) is nonnegative )
for q being object st q in dom (ProjPMap1 (f,x)) holds
0 <= (ProjPMap1 (f,x)) . q

proof

let q be object ; :: thesis: ( q in dom (ProjPMap1 (f,x)) implies 0 <= (ProjPMap1 (f,x)) . q )
assume A2: q in dom (ProjPMap1 (f,x)) ; :: thesis: 0 <= (ProjPMap1 (f,x)) . q
then reconsider y1 = q as Element of X2 ;
(ProjPMap1 (f,x)) . q = f . (x,y1) by A2, Th26;
hence 0 <= (ProjPMap1 (f,x)) . q by A1, SUPINF_2:51; :: thesis: verum

end;

hence ProjPMap1 (f,x) is nonnegative by SUPINF_2:52; :: thesis: ProjPMap2 (f,y) is nonnegative
for p being object st p in dom (ProjPMap2 (f,y)) holds
0 <= (ProjPMap2 (f,y)) . p

proof

let p be object ; :: thesis: ( p in dom (ProjPMap2 (f,y)) implies 0 <= (ProjPMap2 (f,y)) . p )
assume A3: p in dom (ProjPMap2 (f,y)) ; :: thesis: 0 <= (ProjPMap2 (f,y)) . p
then reconsider x1 = p as Element of X1 ;
(ProjPMap2 (f,y)) . p = f . (x1,y) by A3, Th26;
hence 0 <= (ProjPMap2 (f,y)) . p by A1, SUPINF_2:51; :: thesis: verum

end;

hence ProjPMap2 (f,y) is nonnegative by SUPINF_2:52; :: thesis: verum