let X1, X2 be non empty set ; :: thesis: for A being Subset of [:X1,X2:]
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((Xchi (A,[:X1,X2:])),x) = Xchi ((X-section (A,x)),X2) & ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = Xchi ((Y-section (A,y)),X1) )
let A be Subset of [:X1,X2:]; :: thesis: for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 ((Xchi (A,[:X1,X2:])),x) = Xchi ((X-section (A,x)),X2) & ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = Xchi ((Y-section (A,y)),X1) )
let x be Element of X1; :: thesis: for y being Element of X2 holds
( ProjPMap1 ((Xchi (A,[:X1,X2:])),x) = Xchi ((X-section (A,x)),X2) & ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = Xchi ((Y-section (A,y)),X1) )
let y be Element of X2; :: thesis: ( ProjPMap1 ((Xchi (A,[:X1,X2:])),x) = Xchi ((X-section (A,x)),X2) & ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = Xchi ((Y-section (A,y)),X1) )
A3: ( ProjPMap1 ((Xchi (A,[:X1,X2:])),x) = ProjMap1 ((Xchi (A,[:X1,X2:])),x) & ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = ProjMap2 ((Xchi (A,[:X1,X2:])),y) ) by Th27;
for y being Element of X2 holds (ProjMap1 ((Xchi (A,[:X1,X2:])),x)) . y = (Xchi ((X-section (A,x)),X2)) . y
proof
let y be Element of X2; :: thesis: (ProjMap1 ((Xchi (A,[:X1,X2:])),x)) . y = (Xchi ((X-section (A,x)),X2)) . y
a5: [x,y] in [:X1,X2:] by ZFMISC_1:def 2;
a4: (ProjMap1 ((Xchi (A,[:X1,X2:])),x)) . y = (Xchi (A,[:X1,X2:])) . (x,y) by MESFUNC9:def 6;
per cases ( [x,y] in A or not [x,y] in A ) ;
suppose b1: [x,y] in A ; :: thesis: (ProjMap1 ((Xchi (A,[:X1,X2:])),x)) . y = (Xchi ((X-section (A,x)),X2)) . y
then y in X-section (A,x) by Th25;
then ( (ProjMap1 ((Xchi (A,[:X1,X2:])),x)) . y = +infty & (Xchi ((X-section (A,x)),X2)) . y = +infty ) by a4, b1, MEASUR10:def 7;
hence (ProjMap1 ((Xchi (A,[:X1,X2:])),x)) . y = (Xchi ((X-section (A,x)),X2)) . y ; :: thesis: verum
end;
suppose b2: not [x,y] in A ; :: thesis: (ProjMap1 ((Xchi (A,[:X1,X2:])),x)) . y = (Xchi ((X-section (A,x)),X2)) . y
then not y in X-section (A,x) by Th25;
then ( (ProjMap1 ((Xchi (A,[:X1,X2:])),x)) . y = 0 & (Xchi ((X-section (A,x)),X2)) . y = 0 ) by a5, a4, b2, MEASUR10:def 7;
hence (ProjMap1 ((Xchi (A,[:X1,X2:])),x)) . y = (Xchi ((X-section (A,x)),X2)) . y ; :: thesis: verum
end;
end;
end;
hence ProjPMap1 ((Xchi (A,[:X1,X2:])),x) = Xchi ((X-section (A,x)),X2) by A3, FUNCT_2:def 8; :: thesis: ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = Xchi ((Y-section (A,y)),X1)
for x being Element of X1 holds (ProjMap2 ((Xchi (A,[:X1,X2:])),y)) . x = (Xchi ((Y-section (A,y)),X1)) . x
proof
let x be Element of X1; :: thesis: (ProjMap2 ((Xchi (A,[:X1,X2:])),y)) . x = (Xchi ((Y-section (A,y)),X1)) . x
a5: [x,y] in [:X1,X2:] by ZFMISC_1:def 2;
a4: (ProjMap2 ((Xchi (A,[:X1,X2:])),y)) . x = (Xchi (A,[:X1,X2:])) . (x,y) by MESFUNC9:def 7;
per cases ( [x,y] in A or not [x,y] in A ) ;
suppose b1: [x,y] in A ; :: thesis: (ProjMap2 ((Xchi (A,[:X1,X2:])),y)) . x = (Xchi ((Y-section (A,y)),X1)) . x
then x in Y-section (A,y) by Th25;
then ( (ProjMap2 ((Xchi (A,[:X1,X2:])),y)) . x = +infty & (Xchi ((Y-section (A,y)),X1)) . x = +infty ) by a4, b1, MEASUR10:def 7;
hence (ProjMap2 ((Xchi (A,[:X1,X2:])),y)) . x = (Xchi ((Y-section (A,y)),X1)) . x ; :: thesis: verum
end;
suppose b2: not [x,y] in A ; :: thesis: (ProjMap2 ((Xchi (A,[:X1,X2:])),y)) . x = (Xchi ((Y-section (A,y)),X1)) . x
then not x in Y-section (A,y) by Th25;
then ( (ProjMap2 ((Xchi (A,[:X1,X2:])),y)) . x = 0 & (Xchi ((Y-section (A,y)),X1)) . x = 0 ) by a5, a4, b2, MEASUR10:def 7;
hence (ProjMap2 ((Xchi (A,[:X1,X2:])),y)) . x = (Xchi ((Y-section (A,y)),X1)) . x ; :: thesis: verum
end;
end;
end;
hence ProjPMap2 ((Xchi (A,[:X1,X2:])),y) = Xchi ((Y-section (A,y)),X1) by A3, FUNCT_2:def 8; :: thesis: verum