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 nonpositive holds
( ProjPMap1 (f,x) is nonpositive & ProjPMap2 (f,y) is nonpositive )
let x be Element of X1; :: thesis: for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL st f is nonpositive holds
( ProjPMap1 (f,x) is nonpositive & ProjPMap2 (f,y) is nonpositive )
let y be Element of X2; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL st f is nonpositive holds
( ProjPMap1 (f,x) is nonpositive & ProjPMap2 (f,y) is nonpositive )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( f is nonpositive implies ( ProjPMap1 (f,x) is nonpositive & ProjPMap2 (f,y) is nonpositive ) )
assume A1: f is nonpositive ; :: thesis: ( ProjPMap1 (f,x) is nonpositive & ProjPMap2 (f,y) is nonpositive )
for q being set st q in dom (ProjPMap1 (f,x)) holds
0 >= (ProjPMap1 (f,x)) . q
proof
let q be set ; :: 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, MESFUNC5:8; :: thesis: verum
end;
hence ProjPMap1 (f,x) is nonpositive by MESFUNC5:9; :: thesis: ProjPMap2 (f,y) is nonpositive
for p being set st p in dom (ProjPMap2 (f,y)) holds
0 >= (ProjPMap2 (f,y)) . p
proof
let p be set ; :: 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, MESFUNC5:8; :: thesis: verum
end;
hence ProjPMap2 (f,y) is nonpositive by MESFUNC5:9; :: thesis: verum