let X, Y be RealNormSpace; 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 ; 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; 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:]; ( ( 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]
; ( 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) )
hence
dom (f * I) = I " (dom f)
by TARSKI:2; 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; for y being Point of Y holds (f * I) . (y,x) = f . (x,y)
let y be Point of Y; (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
;
verum