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 * () = (f * I) * () & f * () = (f * I) * () )

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 * () = (f * I) * () & f * () = (f * I) * () )

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 * () = (f * I) * () & f * () = (f * I) * () )

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 * () = (f * I) * () & f * () = (f * I) * () ) )

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 * () = (f * I) * () & f * () = (f * I) * () )

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 * () = (f * I) * () & f * () = (f * I) * () )

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 * () = (f * I) * () & f * () = (f * I) * () )

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 * () = (f * I) * () & f * () = (f * I) * () )

let v be Point of [:Y,X:]; :: thesis: ( u in U & u = [a,b] & v = [b,a] implies ( f * () = (f * I) * () & f * () = (f * I) * () ) )
assume A2: ( u in U & u = [a,b] & v = [b,a] ) ; :: thesis: ( f * () = (f * I) * () & f * () = (f * I) * () )
A3: for x being object holds
( x in dom (f * ()) iff x in dom ((f * I) * ()) )
proof
let x be object ; :: thesis: ( x in dom (f * ()) iff x in dom ((f * I) * ()) )
A4: ( x in dom (f * ()) iff ( x in dom () & () . x in dom f ) ) by FUNCT_1:11;
A5: ( x in dom (f * ()) implies x in dom ((f * I) * ()) )
proof
assume A6: x in dom (f * ()) ; :: thesis: x in dom ((f * I) * ())
then A7: x in the carrier of X ;
reconsider x = x as Point of X by A6;
A8: x in dom () by ;
() . x = [(v `1),x] by NDIFF_7:def 2
.= [b,x] by A2 ;
then A9: I . (() . x) = I . (b,x)
.= [x,(u `2)] by A1, A2
.= () . 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 ;
hence x in dom ((f * I) * ()) by ; :: thesis: verum
end;
( x in dom ((f * I) * ()) implies x in dom (f * ()) )
proof
assume A10: x in dom ((f * I) * ()) ; :: thesis: x in dom (f * ())
then A11: ( x in dom () & () . x in dom (f * I) ) by FUNCT_1:11;
reconsider x = x as Point of X by A10;
() . x = [(v `1),x] by NDIFF_7:def 2
.= [b,x] by A2 ;
then I . (() . x) = I . (b,x)
.= [x,(u `2)] by A1, A2
.= () . x by NDIFF_7:def 1 ;
then A12: (reproj1 u) . x in dom f by ;
dom () = the carrier of X by FUNCT_2:def 1;
hence x in dom (f * ()) by ; :: thesis: verum
end;
hence ( x in dom (f * ()) iff x in dom ((f * I) * ()) ) by A5; :: thesis: verum
end;
A13: for y being object holds
( y in dom (f * ()) iff y in dom ((f * I) * ()) )
proof
let y be object ; :: thesis: ( y in dom (f * ()) iff y in dom ((f * I) * ()) )
A14: ( y in dom (f * ()) iff ( y in dom () & () . y in dom f ) ) by FUNCT_1:11;
A15: ( y in dom (f * ()) implies y in dom ((f * I) * ()) )
proof
assume A16: y in dom (f * ()) ; :: thesis: y in dom ((f * I) * ())
then A17: y in the carrier of Y ;
reconsider y = y as Point of Y by A16;
A18: y in dom () by ;
() . y = [y,(v `2)] by NDIFF_7:def 1
.= [y,a] by A2 ;
then A19: I . (() . y) = I . (y,a)
.= [(u `1),y] by A1, A2
.= () . 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 ;
hence y in dom ((f * I) * ()) by ; :: thesis: verum
end;
( y in dom ((f * I) * ()) implies y in dom (f * ()) )
proof
assume A20: y in dom ((f * I) * ()) ; :: thesis: y in dom (f * ())
then A21: ( y in dom () & () . y in dom (f * I) ) by FUNCT_1:11;
reconsider y = y as Point of Y by A20;
() . y = [y,(v `2)] by NDIFF_7:def 1
.= [y,a] by A2 ;
then I . (() . y) = I . (y,a)
.= [(u `1),y] by A1, A2
.= () . y by NDIFF_7:def 2 ;
then A22: (reproj2 u) . y in dom f by ;
dom () = the carrier of Y by FUNCT_2:def 1;
hence y in dom (f * ()) by ; :: thesis: verum
end;
hence ( y in dom (f * ()) iff y in dom ((f * I) * ()) ) by A15; :: thesis: verum
end;
for x being object st x in dom (f * ()) holds
(f * ()) . x = ((f * I) * ()) . x
proof
let x be object ; :: thesis: ( x in dom (f * ()) implies (f * ()) . x = ((f * I) * ()) . x )
assume A23: x in dom (f * ()) ; :: thesis: (f * ()) . x = ((f * I) * ()) . x
then reconsider x = x as Point of X ;
A24: () . x = [x,(u `2)] by NDIFF_7:def 1
.= I . (b,x) by A1, A2
.= I . [(v `1),x] by A2
.= I . (() . 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 () = the carrier of X by FUNCT_2:def 1;
(f * ()) . x = f . (I . (() . x)) by
.= (f * I) . (() . x) by
.= ((f * I) * ()) . x by ;
hence (f * ()) . x = ((f * I) * ()) . x ; :: thesis: verum
end;
hence f * () = (f * I) * () by ; :: thesis: f * () = (f * I) * ()
for y being object st y in dom (f * ()) holds
(f * ()) . y = ((f * I) * ()) . y
proof
let y be object ; :: thesis: ( y in dom (f * ()) implies (f * ()) . y = ((f * I) * ()) . y )
assume A27: y in dom (f * ()) ; :: thesis: (f * ()) . y = ((f * I) * ()) . y
then reconsider y = y as Point of Y ;
A28: () . y = [(u `1),y] by NDIFF_7:def 2
.= I . (y,a) by A1, A2
.= I . [y,(v `2)] by A2
.= I . (() . 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 () = the carrier of Y by FUNCT_2:def 1;
(f * ()) . y = f . (I . (() . y)) by
.= (f * I) . (() . y) by
.= ((f * I) * ()) . y by ;
hence (f * ()) . y = ((f * I) * ()) . y ; :: thesis: verum
end;
hence f * () = (f * I) * () by ; :: thesis: verum