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) )

proof

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;

hence dom (f * I) = I " (dom f) by TARSKI:2; :: thesis: for x being Point of X
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