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)
let x be set ; :: thesis: ( x in dom f implies <:(X --> f):> . x = X --> (f . x) )
assume A3: x in dom f ; :: thesis: <:(X --> f):> . x = X --> (f . x)
then ( <:(X --> f):> . x in rng <:(X --> f):> & rng <:(X --> f):> c= product (rngs (X --> f)) ) by A2, Th49, FUNCT_1:def 5;
then ( <:(X --> f):> . x in product (rngs (X --> f)) & rngs (X --> f) = X --> (rng f) ) by Th36;
then consider g being Function such that
A4: ( <:(X --> f):> . x = g & dom g = dom (X --> (rng f)) & ( for y being set st y in dom (X --> (rng f)) holds
g . y in (X --> (rng f)) . y ) ) by CARD_3:def 5;
A5: ( dom g = X & dom (X --> f) = X & dom (X --> (f . x)) = X ) by A4, FUNCOP_1:19;

now

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

end;

hence <:(X --> f):> . x = X --> (f . x) by A4, A5, FUNCT_1:9; :: thesis: verum