let X, Y, Z be RealNormSpace; :: thesis: for f being PartFunc of [:X,Y:],Z

for U being Subset of [:X,Y:]

for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let f be PartFunc of [:X,Y:],Z; :: thesis: for U being Subset of [:X,Y:]

for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let U be Subset of [:X,Y:]; :: thesis: for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let I be Function of [:Y,X:],[:X,Y:]; :: thesis: ( ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) implies for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) ) )

assume A1: for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ; :: thesis: for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let a be Point of X; :: thesis: for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let b be Point of Y; :: thesis: for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let u be Point of [:X,Y:]; :: thesis: for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let v be Point of [:Y,X:]; :: thesis: ( u in U & u = [a,b] & v = [b,a] implies ( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) ) )

assume A2: ( u in U & u = [a,b] & v = [b,a] ) ; :: thesis: ( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

A3: for x being object holds

( x in dom (f * (reproj1 u)) iff x in dom ((f * I) * (reproj2 v)) )

( y in dom (f * (reproj2 u)) iff y in dom ((f * I) * (reproj1 v)) )

(f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x

for y being object st y in dom (f * (reproj2 u)) holds

(f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y

for U being Subset of [:X,Y:]

for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let f be PartFunc of [:X,Y:],Z; :: thesis: for U being Subset of [:X,Y:]

for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let U be Subset of [:X,Y:]; :: thesis: for I being Function of [:Y,X:],[:X,Y:] st ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) holds

for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let I be Function of [:Y,X:],[:X,Y:]; :: thesis: ( ( for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ) implies for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) ) )

assume A1: for y being Point of Y

for x being Point of X holds I . (y,x) = [x,y] ; :: thesis: for a being Point of X

for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let a be Point of X; :: thesis: for b being Point of Y

for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let b be Point of Y; :: thesis: for u being Point of [:X,Y:]

for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let u be Point of [:X,Y:]; :: thesis: for v being Point of [:Y,X:] st u in U & u = [a,b] & v = [b,a] holds

( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

let v be Point of [:Y,X:]; :: thesis: ( u in U & u = [a,b] & v = [b,a] implies ( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) ) )

assume A2: ( u in U & u = [a,b] & v = [b,a] ) ; :: thesis: ( f * (reproj1 u) = (f * I) * (reproj2 v) & f * (reproj2 u) = (f * I) * (reproj1 v) )

A3: for x being object holds

( x in dom (f * (reproj1 u)) iff x in dom ((f * I) * (reproj2 v)) )

proof

A13:
for y being object holds
let x be object ; :: thesis: ( x in dom (f * (reproj1 u)) iff x in dom ((f * I) * (reproj2 v)) )

A4: ( x in dom (f * (reproj1 u)) iff ( x in dom (reproj1 u) & (reproj1 u) . x in dom f ) ) by FUNCT_1:11;

A5: ( x in dom (f * (reproj1 u)) implies x in dom ((f * I) * (reproj2 v)) )

end;A4: ( x in dom (f * (reproj1 u)) iff ( x in dom (reproj1 u) & (reproj1 u) . x in dom f ) ) by FUNCT_1:11;

A5: ( x in dom (f * (reproj1 u)) implies x in dom ((f * I) * (reproj2 v)) )

proof

( x in dom ((f * I) * (reproj2 v)) implies x in dom (f * (reproj1 u)) )
assume A6:
x in dom (f * (reproj1 u))
; :: thesis: x in dom ((f * I) * (reproj2 v))

then A7: x in the carrier of X ;

reconsider x = x as Point of X by A6;

A8: x in dom (reproj2 v) by A7, FUNCT_2:def 1;

(reproj2 v) . x = [(v `1),x] by NDIFF_7:def 2

.= [b,x] by A2 ;

then A9: I . ((reproj2 v) . x) = I . (b,x)

.= [x,(u `2)] by A1, A2

.= (reproj1 u) . x by NDIFF_7:def 1 ;

(reproj2 v) . x in the carrier of [:Y,X:] ;

then (reproj2 v) . x in dom I by FUNCT_2:def 1;

then (reproj2 v) . x in dom (f * I) by A4, A6, A9, FUNCT_1:11;

hence x in dom ((f * I) * (reproj2 v)) by A8, FUNCT_1:11; :: thesis: verum

end;then A7: x in the carrier of X ;

reconsider x = x as Point of X by A6;

A8: x in dom (reproj2 v) by A7, FUNCT_2:def 1;

(reproj2 v) . x = [(v `1),x] by NDIFF_7:def 2

.= [b,x] by A2 ;

then A9: I . ((reproj2 v) . x) = I . (b,x)

.= [x,(u `2)] by A1, A2

.= (reproj1 u) . x by NDIFF_7:def 1 ;

(reproj2 v) . x in the carrier of [:Y,X:] ;

then (reproj2 v) . x in dom I by FUNCT_2:def 1;

then (reproj2 v) . x in dom (f * I) by A4, A6, A9, FUNCT_1:11;

hence x in dom ((f * I) * (reproj2 v)) by A8, FUNCT_1:11; :: thesis: verum

proof

hence
( x in dom (f * (reproj1 u)) iff x in dom ((f * I) * (reproj2 v)) )
by A5; :: thesis: verum
assume A10:
x in dom ((f * I) * (reproj2 v))
; :: thesis: x in dom (f * (reproj1 u))

then A11: ( x in dom (reproj2 v) & (reproj2 v) . x in dom (f * I) ) by FUNCT_1:11;

reconsider x = x as Point of X by A10;

(reproj2 v) . x = [(v `1),x] by NDIFF_7:def 2

.= [b,x] by A2 ;

then I . ((reproj2 v) . x) = I . (b,x)

.= [x,(u `2)] by A1, A2

.= (reproj1 u) . x by NDIFF_7:def 1 ;

then A12: (reproj1 u) . x in dom f by A11, FUNCT_1:11;

dom (reproj1 u) = the carrier of X by FUNCT_2:def 1;

hence x in dom (f * (reproj1 u)) by A12, FUNCT_1:11; :: thesis: verum

end;then A11: ( x in dom (reproj2 v) & (reproj2 v) . x in dom (f * I) ) by FUNCT_1:11;

reconsider x = x as Point of X by A10;

(reproj2 v) . x = [(v `1),x] by NDIFF_7:def 2

.= [b,x] by A2 ;

then I . ((reproj2 v) . x) = I . (b,x)

.= [x,(u `2)] by A1, A2

.= (reproj1 u) . x by NDIFF_7:def 1 ;

then A12: (reproj1 u) . x in dom f by A11, FUNCT_1:11;

dom (reproj1 u) = the carrier of X by FUNCT_2:def 1;

hence x in dom (f * (reproj1 u)) by A12, FUNCT_1:11; :: thesis: verum

( y in dom (f * (reproj2 u)) iff y in dom ((f * I) * (reproj1 v)) )

proof

for x being object st x in dom (f * (reproj1 u)) holds
let y be object ; :: thesis: ( y in dom (f * (reproj2 u)) iff y in dom ((f * I) * (reproj1 v)) )

A14: ( y in dom (f * (reproj2 u)) iff ( y in dom (reproj2 u) & (reproj2 u) . y in dom f ) ) by FUNCT_1:11;

A15: ( y in dom (f * (reproj2 u)) implies y in dom ((f * I) * (reproj1 v)) )

end;A14: ( y in dom (f * (reproj2 u)) iff ( y in dom (reproj2 u) & (reproj2 u) . y in dom f ) ) by FUNCT_1:11;

A15: ( y in dom (f * (reproj2 u)) implies y in dom ((f * I) * (reproj1 v)) )

proof

( y in dom ((f * I) * (reproj1 v)) implies y in dom (f * (reproj2 u)) )
assume A16:
y in dom (f * (reproj2 u))
; :: thesis: y in dom ((f * I) * (reproj1 v))

then A17: y in the carrier of Y ;

reconsider y = y as Point of Y by A16;

A18: y in dom (reproj1 v) by A17, FUNCT_2:def 1;

(reproj1 v) . y = [y,(v `2)] by NDIFF_7:def 1

.= [y,a] by A2 ;

then A19: I . ((reproj1 v) . y) = I . (y,a)

.= [(u `1),y] by A1, A2

.= (reproj2 u) . y by NDIFF_7:def 2 ;

(reproj1 v) . y in the carrier of [:Y,X:] ;

then (reproj1 v) . y in dom I by FUNCT_2:def 1;

then (reproj1 v) . y in dom (f * I) by A14, A16, A19, FUNCT_1:11;

hence y in dom ((f * I) * (reproj1 v)) by A18, FUNCT_1:11; :: thesis: verum

end;then A17: y in the carrier of Y ;

reconsider y = y as Point of Y by A16;

A18: y in dom (reproj1 v) by A17, FUNCT_2:def 1;

(reproj1 v) . y = [y,(v `2)] by NDIFF_7:def 1

.= [y,a] by A2 ;

then A19: I . ((reproj1 v) . y) = I . (y,a)

.= [(u `1),y] by A1, A2

.= (reproj2 u) . y by NDIFF_7:def 2 ;

(reproj1 v) . y in the carrier of [:Y,X:] ;

then (reproj1 v) . y in dom I by FUNCT_2:def 1;

then (reproj1 v) . y in dom (f * I) by A14, A16, A19, FUNCT_1:11;

hence y in dom ((f * I) * (reproj1 v)) by A18, FUNCT_1:11; :: thesis: verum

proof

hence
( y in dom (f * (reproj2 u)) iff y in dom ((f * I) * (reproj1 v)) )
by A15; :: thesis: verum
assume A20:
y in dom ((f * I) * (reproj1 v))
; :: thesis: y in dom (f * (reproj2 u))

then A21: ( y in dom (reproj1 v) & (reproj1 v) . y in dom (f * I) ) by FUNCT_1:11;

reconsider y = y as Point of Y by A20;

(reproj1 v) . y = [y,(v `2)] by NDIFF_7:def 1

.= [y,a] by A2 ;

then I . ((reproj1 v) . y) = I . (y,a)

.= [(u `1),y] by A1, A2

.= (reproj2 u) . y by NDIFF_7:def 2 ;

then A22: (reproj2 u) . y in dom f by A21, FUNCT_1:11;

dom (reproj2 u) = the carrier of Y by FUNCT_2:def 1;

hence y in dom (f * (reproj2 u)) by A22, FUNCT_1:11; :: thesis: verum

end;then A21: ( y in dom (reproj1 v) & (reproj1 v) . y in dom (f * I) ) by FUNCT_1:11;

reconsider y = y as Point of Y by A20;

(reproj1 v) . y = [y,(v `2)] by NDIFF_7:def 1

.= [y,a] by A2 ;

then I . ((reproj1 v) . y) = I . (y,a)

.= [(u `1),y] by A1, A2

.= (reproj2 u) . y by NDIFF_7:def 2 ;

then A22: (reproj2 u) . y in dom f by A21, FUNCT_1:11;

dom (reproj2 u) = the carrier of Y by FUNCT_2:def 1;

hence y in dom (f * (reproj2 u)) by A22, FUNCT_1:11; :: thesis: verum

(f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x

proof

hence
f * (reproj1 u) = (f * I) * (reproj2 v)
by A3, FUNCT_1:2, TARSKI:2; :: thesis: f * (reproj2 u) = (f * I) * (reproj1 v)
let x be object ; :: thesis: ( x in dom (f * (reproj1 u)) implies (f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x )

assume A23: x in dom (f * (reproj1 u)) ; :: thesis: (f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x

then reconsider x = x as Point of X ;

A24: (reproj1 u) . x = [x,(u `2)] by NDIFF_7:def 1

.= I . (b,x) by A1, A2

.= I . [(v `1),x] by A2

.= I . ((reproj2 v) . x) by NDIFF_7:def 2 ;

(reproj2 v) . x in the carrier of [:Y,X:] ;

then A25: (reproj2 v) . x in dom I by FUNCT_2:def 1;

A26: dom (reproj2 v) = the carrier of X by FUNCT_2:def 1;

(f * (reproj1 u)) . x = f . (I . ((reproj2 v) . x)) by A23, A24, FUNCT_1:12

.= (f * I) . ((reproj2 v) . x) by A25, FUNCT_1:13

.= ((f * I) * (reproj2 v)) . x by A26, FUNCT_1:13 ;

hence (f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x ; :: thesis: verum

end;assume A23: x in dom (f * (reproj1 u)) ; :: thesis: (f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x

then reconsider x = x as Point of X ;

A24: (reproj1 u) . x = [x,(u `2)] by NDIFF_7:def 1

.= I . (b,x) by A1, A2

.= I . [(v `1),x] by A2

.= I . ((reproj2 v) . x) by NDIFF_7:def 2 ;

(reproj2 v) . x in the carrier of [:Y,X:] ;

then A25: (reproj2 v) . x in dom I by FUNCT_2:def 1;

A26: dom (reproj2 v) = the carrier of X by FUNCT_2:def 1;

(f * (reproj1 u)) . x = f . (I . ((reproj2 v) . x)) by A23, A24, FUNCT_1:12

.= (f * I) . ((reproj2 v) . x) by A25, FUNCT_1:13

.= ((f * I) * (reproj2 v)) . x by A26, FUNCT_1:13 ;

hence (f * (reproj1 u)) . x = ((f * I) * (reproj2 v)) . x ; :: thesis: verum

for y being object st y in dom (f * (reproj2 u)) holds

(f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y

proof

hence
f * (reproj2 u) = (f * I) * (reproj1 v)
by A13, FUNCT_1:2, TARSKI:2; :: thesis: verum
let y be object ; :: thesis: ( y in dom (f * (reproj2 u)) implies (f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y )

assume A27: y in dom (f * (reproj2 u)) ; :: thesis: (f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y

then reconsider y = y as Point of Y ;

A28: (reproj2 u) . y = [(u `1),y] by NDIFF_7:def 2

.= I . (y,a) by A1, A2

.= I . [y,(v `2)] by A2

.= I . ((reproj1 v) . y) by NDIFF_7:def 1 ;

(reproj1 v) . y in the carrier of [:Y,X:] ;

then A29: (reproj1 v) . y in dom I by FUNCT_2:def 1;

A30: dom (reproj1 v) = the carrier of Y by FUNCT_2:def 1;

(f * (reproj2 u)) . y = f . (I . ((reproj1 v) . y)) by A27, A28, FUNCT_1:12

.= (f * I) . ((reproj1 v) . y) by A29, FUNCT_1:13

.= ((f * I) * (reproj1 v)) . y by A30, FUNCT_1:13 ;

hence (f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y ; :: thesis: verum

end;assume A27: y in dom (f * (reproj2 u)) ; :: thesis: (f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y

then reconsider y = y as Point of Y ;

A28: (reproj2 u) . y = [(u `1),y] by NDIFF_7:def 2

.= I . (y,a) by A1, A2

.= I . [y,(v `2)] by A2

.= I . ((reproj1 v) . y) by NDIFF_7:def 1 ;

(reproj1 v) . y in the carrier of [:Y,X:] ;

then A29: (reproj1 v) . y in dom I by FUNCT_2:def 1;

A30: dom (reproj1 v) = the carrier of Y by FUNCT_2:def 1;

(f * (reproj2 u)) . y = f . (I . ((reproj1 v) . y)) by A27, A28, FUNCT_1:12

.= (f * I) . ((reproj1 v) . y) by A29, FUNCT_1:13

.= ((f * I) * (reproj1 v)) . y by A30, FUNCT_1:13 ;

hence (f * (reproj2 u)) . y = ((f * I) * (reproj1 v)) . y ; :: thesis: verum