let X, Y be RealNormSpace; :: thesis: for Z being non empty set

for f being PartFunc of [:X,Y:],Z

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

( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )

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

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

( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )

let f be PartFunc of [:X,Y:],Z; :: 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

( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )

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 ( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) ) )

assume A1: for x being Point of Y

for y being Point of X holds I . (x,y) = [y,x] ; :: thesis: ( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )

for w being object holds

( w in dom (f * I) iff w in I " (dom f) )

for y being Point of Y holds (f * I) . (y,x) = f . (x,y)

let x be Point of X; :: thesis: for y being Point of Y holds (f * I) . (y,x) = f . (x,y)

let y be Point of Y; :: thesis: (f * I) . (y,x) = f . (x,y)

[y,x] in the carrier of [:Y,X:] ;

then [y,x] in dom I by FUNCT_2:def 1;

hence (f * I) . (y,x) = f . (I . (y,x)) by FUNCT_1:13

.= f . (x,y) by A1 ;

:: thesis: verum

for f being PartFunc of [:X,Y:],Z

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

( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )

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

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

( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )

let f be PartFunc of [:X,Y:],Z; :: 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

( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )

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 ( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) ) )

assume A1: for x being Point of Y

for y being Point of X holds I . (x,y) = [y,x] ; :: thesis: ( dom (f * I) = I " (dom f) & ( for x being Point of X

for y being Point of Y holds (f * I) . (y,x) = f . (x,y) ) )

for w being object holds

( w in dom (f * I) iff w in I " (dom f) )

proof

hence
dom (f * I) = I " (dom f)
by TARSKI:2; :: thesis: for x being Point of X
let w be object ; :: thesis: ( w in dom (f * I) iff w in I " (dom f) )

( w in dom (f * I) iff ( w in dom I & I . w in dom f ) ) by FUNCT_1:11;

hence ( w in dom (f * I) iff w in I " (dom f) ) by FUNCT_1:def 7; :: thesis: verum

end;( w in dom (f * I) iff ( w in dom I & I . w in dom f ) ) by FUNCT_1:11;

hence ( w in dom (f * I) iff w in I " (dom f) ) by FUNCT_1:def 7; :: thesis: verum

for y being Point of Y holds (f * I) . (y,x) = f . (x,y)

let x be Point of X; :: thesis: for y being Point of Y holds (f * I) . (y,x) = f . (x,y)

let y be Point of Y; :: thesis: (f * I) . (y,x) = f . (x,y)

[y,x] in the carrier of [:Y,X:] ;

then [y,x] in dom I by FUNCT_2:def 1;

hence (f * I) . (y,x) = f . (I . (y,x)) by FUNCT_1:13

.= f . (x,y) by A1 ;

:: thesis: verum