let X1, X2 be non empty set ; for x being Element of X1
for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL
for er being ExtReal holds
( ( [x,y] in dom f & f . (x,y) = er implies ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er ) ) & ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er implies ( [x,y] in dom f & f . (x,y) = er ) ) & ( [x,y] in dom f & f . (x,y) = er implies ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er ) ) & ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er implies ( [x,y] in dom f & f . (x,y) = er ) ) )
let x be Element of X1; for y being Element of X2
for f being PartFunc of [:X1,X2:],ExtREAL
for er being ExtReal holds
( ( [x,y] in dom f & f . (x,y) = er implies ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er ) ) & ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er implies ( [x,y] in dom f & f . (x,y) = er ) ) & ( [x,y] in dom f & f . (x,y) = er implies ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er ) ) & ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er implies ( [x,y] in dom f & f . (x,y) = er ) ) )
let y be Element of X2; for f being PartFunc of [:X1,X2:],ExtREAL
for er being ExtReal holds
( ( [x,y] in dom f & f . (x,y) = er implies ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er ) ) & ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er implies ( [x,y] in dom f & f . (x,y) = er ) ) & ( [x,y] in dom f & f . (x,y) = er implies ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er ) ) & ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er implies ( [x,y] in dom f & f . (x,y) = er ) ) )
let f be PartFunc of [:X1,X2:],ExtREAL; for er being ExtReal holds
( ( [x,y] in dom f & f . (x,y) = er implies ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er ) ) & ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = er implies ( [x,y] in dom f & f . (x,y) = er ) ) & ( [x,y] in dom f & f . (x,y) = er implies ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er ) ) & ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = er implies ( [x,y] in dom f & f . (x,y) = er ) ) )
let a be ExtReal; ( ( [x,y] in dom f & f . (x,y) = a implies ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = a ) ) & ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = a implies ( [x,y] in dom f & f . (x,y) = a ) ) & ( [x,y] in dom f & f . (x,y) = a implies ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = a ) ) & ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = a implies ( [x,y] in dom f & f . (x,y) = a ) ) )
hereby ( ( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = a implies ( [x,y] in dom f & f . (x,y) = a ) ) & ( [x,y] in dom f & f . (x,y) = a implies ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = a ) ) & ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = a implies ( [x,y] in dom f & f . (x,y) = a ) ) )
assume that A2:
[x,y] in dom f
and A3:
f . (
x,
y)
= a
;
( y in dom (ProjPMap1 (f,x)) & (ProjPMap1 (f,x)) . y = a )
y in X-section (
(dom f),
x)
by A2, Th25;
hence
y in dom (ProjPMap1 (f,x))
by Def3;
(ProjPMap1 (f,x)) . y = ahence
(ProjPMap1 (f,x)) . y = a
by A3, Th26;
verum
end;
hereby ( [x,y] in dom f & f . (x,y) = a iff ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = a ) )
assume that A4:
y in dom (ProjPMap1 (f,x))
and A5:
(ProjPMap1 (f,x)) . y = a
;
( [x,y] in dom f & f . (x,y) = a )
y in X-section (
(dom f),
x)
by A4, Def3;
hence
[x,y] in dom f
by Th25;
f . (x,y) = athus
f . (
x,
y)
= a
by A4, A5, Th26;
verum
end;
hereby ( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = a implies ( [x,y] in dom f & f . (x,y) = a ) )
assume that A6:
[x,y] in dom f
and A7:
f . (
x,
y)
= a
;
( x in dom (ProjPMap2 (f,y)) & (ProjPMap2 (f,y)) . x = a )
x in Y-section (
(dom f),
y)
by A6, Th25;
hence
x in dom (ProjPMap2 (f,y))
by Def4;
(ProjPMap2 (f,y)) . x = ahence
(ProjPMap2 (f,y)) . x = a
by A7, Th26;
verum
end;
assume that
A8:
x in dom (ProjPMap2 (f,y))
and
A9:
(ProjPMap2 (f,y)) . x = a
; ( [x,y] in dom f & f . (x,y) = a )
x in Y-section ((dom f),y)
by A8, Def4;
hence
[x,y] in dom f
by Th25; f . (x,y) = a
thus
f . (x,y) = a
by A8, A9, Th26; verum