let X be set ; 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; ( 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 <> {}
; ( 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
; 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 ; ( x in dom f implies <:(X --> f):> . x = X --> (f . x) )
assume A4:
x in dom f
; <:(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 for y being object st y in X holds
g . y = (X --> (f . x)) . ylet y be
object ;
( y in X implies g . y = (X --> (f . x)) . y )assume A10:
y in X
;
g . y = (X --> (f . x)) . ythen
(
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;
verum end;
thus
<:(X --> f):> . x = X --> (f . x)
by A5, A7, A9; verum