let X be set ; :: thesis: for f being Function st X <> {} holds
( dom <:(X --> f):> = dom f & ( for x being object 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 object st x in dom f holds
<:(X --> f):> . x = X --> (f . x) ) ) )
assume A1: X <> {} ; :: thesis: ( dom <:(X --> f):> = dom f & ( for x being object st x in dom f holds
<:(X --> f):> . x = X --> (f . x) ) )
thus A2: dom <:(X --> f):> = meet (doms (X --> f)) by Th25
.= meet (X --> (dom f)) by Th20
.= dom f by A1, Th23 ; :: thesis: for x being object 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 Th20, Th25;
let x be object ; :: 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 3;
then consider g being Function such that
A5: <:(X --> f):> . x = g and
A6: dom g = dom (X --> (rng f)) and
for y being object 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;
A8: dom (X --> f) = X ;

A9: now :: thesis: for y being object st y in X holds
g . y = (X --> (f . x)) . y

let y be object ; :: 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, Th26, FUNCOP_1:7;
then g . y = f . x by A4, A8, A10, FUNCT_5:38;
hence g . y = (X --> (f . x)) . y by A10, FUNCOP_1:7; :: thesis: verum

end;

thus <:(X --> f):> . x = X --> (f . x) by A5, A7, A9; :: thesis: verum