let X, Y be set ; :: thesis:
let F be Function-yielding Function; :: thesis:
set FF = dom F;
A1: dom (doms F) = dom F by FUNCT_6:59;
let x, y be object ; :: thesis:
assume A2: ( F is Funcs (X,Y) -valued or y in dom <:F:> ) ; :: thesis:

per cases by A2;

suppose ( y in dom <:F:> & x in dom F ) ; :: thesis:

hence (F . x) . y = (<:F:> . y) . x by FUNCT_6:34; :: thesis:

end;

suppose A3: ( y in dom <:F:> & not x in dom F ) ; :: thesis:

then dom (<:F:> . y) = dom F by FUNCT_6:31;
then A4: (<:F:> . y) . x = {} by A3, FUNCT_1:def 2;
F . x = {} by A3, FUNCT_1:def 2;
hence (F . x) . y = (<:F:> . y) . x by A4; :: thesis:

end;

suppose A5: ( not y in dom <:F:> & x in dom F & F is Funcs (X,Y) -valued ) ; :: thesis:

then A6: <:F:> . y = {} by FUNCT_1:def 2;
A7: rng F c= Funcs (X,Y) by RELAT_1:def 19, A5;
F . x in rng F by A5, FUNCT_1:def 3;
then consider Fx being Function such that
A8: Fx = F . x and
A9: dom Fx = X and
rng Fx c= Y by A7, FUNCT_2:def 2;

let x be object ; :: thesis:
assume A10: x in dom F ; :: thesis:
then F . x in rng F by FUNCT_1:def 3;
then ex Fx being Function st
( Fx = F . x & dom Fx = X & rng Fx c= Y ) by A7, FUNCT_2:def 2;
hence (doms F) . x = X by A10, FUNCT_6:22; :: thesis:

end;

then doms F = (dom F) --> X by A1, FUNCOP_1:11;
then dom <:F:> = meet ((dom F) --> X) by FUNCT_6:29;
then dom <:F:> = X by A5, FUNCT_6:27;
then Fx . y = {} by A9, A5, FUNCT_1:def 2;
hence (F . x) . y = (<:F:> . y) . x by A6, A8; :: thesis:

end;

suppose A11: ( not y in dom <:F:> & not x in dom F ) ; :: thesis:

then A12: F . x = {} by FUNCT_1:def 2;
A13: {} . x = {} ;
<:F:> . y = {} by A11, FUNCT_1:def 2;
hence (F . x) . y = (<:F:> . y) . x by A12, A13; :: thesis:

end;

end;