let x be set ; :: thesis: for f, g being Function st x in dom <:f:> & g = <:f:> . x holds
( dom g = f " (SubFuncs (rng f)) & ( for y being set st y in dom g holds
( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) ) )
let f, g be Function; :: thesis: ( x in dom <:f:> & g = <:f:> . x implies ( dom g = f " (SubFuncs (rng f)) & ( for y being set st y in dom g holds
( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) ) ) )
A1: ( rng <:f:> c= product (rngs f) & dom (rngs f) = f " (SubFuncs (rng f)) ) by Def3, Th49;
assume A2: ( x in dom <:f:> & g = <:f:> . x ) ; :: thesis: ( dom g = f " (SubFuncs (rng f)) & ( for y being set st y in dom g holds
( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) ) )
then g in rng <:f:> by FUNCT_1:def 3;
hence dom g = f " (SubFuncs (rng f)) by A1, CARD_3:9; :: thesis: for y being set st y in dom g holds
( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) )
let y be set ; :: thesis: ( y in dom g implies ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) )
assume A3: y in dom g ; :: thesis: ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) )
A4: [x,y] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) by A2, A3, FUNCT_5:31;
then [x,y] in (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] by RELAT_1:61;
then A5: [x,y] in dom (uncurry' f) by XBOOLE_0:def 4;
g . y = ((uncurry' f) | [:(meet (doms f)),(dom f):]) . (x,y) by A2, A3, FUNCT_5:31;
then A6: g . y = (uncurry' f) . (x,y) by A4, FUNCT_1:47;
~ (uncurry f) = uncurry' f by FUNCT_5:def 4;
hence ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . (y,x) ) by A6, A5, FUNCT_4:42, FUNCT_4:43; :: thesis: verum