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 ) ) ) )
assume A1: ( 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:> & rng <:f:> c= product (rngs f) ) by Th49, FUNCT_1:def 5;
then ( g in product (rngs f) & dom (rngs f) = f " (SubFuncs (rng f)) ) by Def3;
hence dom g = f " (SubFuncs (rng f)) by 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 A2: y in dom g ; :: thesis: ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . y,x )
( g . y = ((uncurry' f) | [:(meet (doms f)),(dom f):]) . x,y & [x,y] in dom ((uncurry' f) | [:(meet (doms f)),(dom f):]) ) by A1, A2, FUNCT_5:38;
then A3: ( g . y = (uncurry' f) . x,y & [x,y] in (dom (uncurry' f)) /\ [:(meet (doms f)),(dom f):] ) by FUNCT_1:70, RELAT_1:90;
then ( [x,y] in dom (uncurry' f) & ~ (uncurry f) = uncurry' f ) by FUNCT_5:def 6, XBOOLE_0:def 4;
hence ( [y,x] in dom (uncurry f) & g . y = (uncurry f) . y,x ) by A3, FUNCT_4:43, FUNCT_4:44; :: thesis: verum