let X be set ; :: thesis: for f being Function st X <> {} holds
( dom <:(X --> f):> = dom f & ( for x being set st x in dom f holds
<:(X --> f):> . x = X --> (f . x) ) )
let f be Function; :: thesis: ( X <> {} implies ( dom <:(X --> f):> = dom f & ( for x being set st x in dom f holds
<:(X --> f):> . x = X --> (f . x) ) ) )
assume A1: X <> {} ; :: thesis: ( dom <:(X --> f):> = dom f & ( for x being set st x in dom f holds
<:(X --> f):> . x = X --> (f . x) ) )
thus A2: dom <:(X --> f):> = meet (doms (X --> f)) by Th49
.= meet (X --> (dom f)) by Th36
.= dom f by A1, Th43 ; :: thesis: for x being set st x in dom f holds
<:(X --> f):> . x = X --> (f . x)
A3: ( rng <:(X --> f):> c= product (rngs (X --> f)) & rngs (X --> f) = X --> (rng f) ) by Th36, Th49;
let x be set ; :: thesis: ( x in dom f implies <:(X --> f):> . x = X --> (f . x) )
assume A4: x in dom f ; :: thesis: <:(X --> f):> . x = X --> (f . x)
then <:(X --> f):> . x in rng <:(X --> f):> by A2, FUNCT_1:def 5;
then consider g being Function such that
A5: <:(X --> f):> . x = g and
A6: dom g = dom (X --> (rng f)) and
for y being set st y in dom (X --> (rng f)) holds
g . y in (X --> (rng f)) . y by A3, CARD_3:def 5;
A7: dom g = X by A6, FUNCOP_1:19;
A8: dom (X --> f) = X by FUNCOP_1:19;

A9: now

let y be set ; :: thesis: ( y in X implies g . y = (X --> (f . x)) . y )
assume A10: y in X ; :: thesis: g . y = (X --> (f . x)) . y
then ( g . y = (uncurry (X --> f)) . (y,x) & (X --> f) . y = f ) by A2, A4, A5, A7, Th51, FUNCOP_1:13;
then g . y = f . x by A4, A8, A10, FUNCT_5:45;
hence g . y = (X --> (f . x)) . y by A10, FUNCOP_1:13; :: thesis: verum

end;

dom (X --> (f . x)) = X by FUNCOP_1:19;
hence <:(X --> f):> . x = X --> (f . x) by A5, A7, A9, FUNCT_1:9; :: thesis: verum