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

per cases ( ( y in dom <:F:> & x in dom F ) or ( y in dom <:F:> & not x in dom F ) or ( not y in dom <:F:> & x in dom F & F is Funcs (X,Y) -valued ) or ( not y in dom <:F:> & not x in dom F ) ) by A2;

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

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

end;

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

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: verum

end;

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

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;

now :: thesis: for x being object st x in dom F holds
(doms F) . x = X

let x be object ; :: thesis: ( x in dom F implies (doms F) . x = X )
assume A10: x in dom F ; :: thesis: (doms F) . x = X
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: verum

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: verum

end;

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

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: verum

end;

end;