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 5;
hence dom g = f " (SubFuncs (rng f)) by A1, CARD_3:18; :: 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:38;
then [x,y] in (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] by RELAT_1:90;
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:38;
then A6: g . y = (uncurry' f) . x,y by A4, FUNCT_1:70;
~ (uncurry f) = uncurry' f by FUNCT_5:def 6;
hence ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . y,x ) by A6, A5, FUNCT_4:43, FUNCT_4:44; :: thesis: verum