let C be non empty with_binary_products with_exponential_objects category; :: thesis: for a, b, c being Object of C st Hom ((c [x] a),b) <> {} holds
ex L being Function of (Hom ((c [x] a),b)),(Hom (c,(b |^ a))) st
( ( for f being Morphism of c [x] a,b
for h being Morphism of c,b |^ a st h = L . f holds
(eval (a,b)) * (h [x] (id- a)) = f ) & L is bijective )
let a, b, c be Object of C; :: thesis: ( Hom ((c [x] a),b) <> {} implies ex L being Function of (Hom ((c [x] a),b)),(Hom (c,(b |^ a))) st
( ( for f being Morphism of c [x] a,b
for h being Morphism of c,b |^ a st h = L . f holds
(eval (a,b)) * (h [x] (id- a)) = f ) & L is bijective ) )
assume A1: Hom ((c [x] a),b) <> {} ; :: thesis: ex L being Function of (Hom ((c [x] a),b)),(Hom (c,(b |^ a))) st
( ( for f being Morphism of c [x] a,b
for h being Morphism of c,b |^ a st h = L . f holds
(eval (a,b)) * (h [x] (id- a)) = f ) & L is bijective )
A2: ( Hom (((b |^ a) [x] a),b) <> {} & b |^ a, eval (a,b) is_exponent_of a,b ) by Th70;
defpred S₁[ object , object ] means for f being Morphism of c [x] a,b st f = $1 holds
ex h being Morphism of c,b |^ a st
( h = $2 & f = (eval (a,b)) * (h [x] (id- a)) & ( for h1 being Morphism of c,b |^ a st f = (eval (a,b)) * (h1 [x] (id- a)) holds
h = h1 ) );
A4: for x being object st x in Hom ((c [x] a),b) holds
ex y being object st
( y in Hom (c,(b |^ a)) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in Hom ((c [x] a),b) implies ex y being object st
( y in Hom (c,(b |^ a)) & S₁[x,y] ) )
assume A5: x in Hom ((c [x] a),b) ; :: thesis: ex y being object st
( y in Hom (c,(b |^ a)) & S₁[x,y] )
reconsider f = x as Morphism of c [x] a,b by A5, CAT_7:def 3;
consider y being Morphism of c,b |^ a such that
A6: ( f = (eval (a,b)) * (y [x] (id- a)) & ( for h1 being Morphism of c,b |^ a st f = (eval (a,b)) * (h1 [x] (id- a)) holds
y = h1 ) ) by A2, A1, Def29;
take y ; :: thesis: ( y in Hom (c,(b |^ a)) & S₁[x,y] )
Hom (c,(b |^ a)) <> {} by A2, A1, Def29;
hence y in Hom (c,(b |^ a)) by CAT_7:def 3; :: thesis: S₁[x,y]
thus S₁[x,y] by A6; :: thesis: verum

end;

consider L being Function of (Hom ((c [x] a),b)),(Hom (c,(b |^ a))) such that
A7: for x being object st x in Hom ((c [x] a),b) holds
S₁[x,L . x] from FUNCT_2:sch 1(A4);
take L ; :: thesis: ( ( for f being Morphism of c [x] a,b
for h being Morphism of c,b |^ a st h = L . f holds
(eval (a,b)) * (h [x] (id- a)) = f ) & L is bijective )
A8: ex y being object st y in Hom (c,(b |^ a))

proof

consider x being object such that
A9: x in Hom ((c [x] a),b) by A1, XBOOLE_0:def 1;
consider y being object such that
A10: ( y in Hom (c,(b |^ a)) & S₁[x,y] ) by A9, A4;
take y ; :: thesis: y in Hom (c,(b |^ a))
thus y in Hom (c,(b |^ a)) by A10; :: thesis: verum

end;

thus for f being Morphism of c [x] a,b
for h being Morphism of c,b |^ a st h = L . f holds
(eval (a,b)) * (h [x] (id- a)) = f :: thesis: L is bijective

proof

let f be Morphism of c [x] a,b; :: thesis: for h being Morphism of c,b |^ a st h = L . f holds
(eval (a,b)) * (h [x] (id- a)) = f
f in Hom ((c [x] a),b) by A1, CAT_7:def 3;
then consider h0 being Morphism of c,b |^ a such that
A11: ( h0 = L . f & f = (eval (a,b)) * (h0 [x] (id- a)) & ( for h1 being Morphism of c,b |^ a st f = (eval (a,b)) * (h1 [x] (id- a)) holds
h0 = h1 ) ) by A7;
let h be Morphism of c,b |^ a; :: thesis: ( h = L . f implies (eval (a,b)) * (h [x] (id- a)) = f )
assume h = L . f ; :: thesis: (eval (a,b)) * (h [x] (id- a)) = f
hence (eval (a,b)) * (h [x] (id- a)) = f by A11; :: thesis: verum

end;

for x1, x2 being object st x1 in Hom ((c [x] a),b) & x2 in Hom ((c [x] a),b) & L . x1 = L . x2 holds
x1 = x2

proof

let x1, x2 be object ; :: thesis: ( x1 in Hom ((c [x] a),b) & x2 in Hom ((c [x] a),b) & L . x1 = L . x2 implies x1 = x2 )
assume A12: x1 in Hom ((c [x] a),b) ; :: thesis: ( not x2 in Hom ((c [x] a),b) or not L . x1 = L . x2 or x1 = x2 )
then reconsider f1 = x1 as Morphism of c [x] a,b by CAT_7:def 3;
consider h1 being Morphism of c,b |^ a such that
A13: ( h1 = L . x1 & f1 = (eval (a,b)) * (h1 [x] (id- a)) & ( for h0 being Morphism of c,b |^ a st f1 = (eval (a,b)) * (h0 [x] (id- a)) holds
h1 = h0 ) ) by A12, A7;
assume A14: x2 in Hom ((c [x] a),b) ; :: thesis: ( not L . x1 = L . x2 or x1 = x2 )
then reconsider f2 = x2 as Morphism of c [x] a,b by CAT_7:def 3;
consider h2 being Morphism of c,b |^ a such that
A15: ( h2 = L . x2 & f2 = (eval (a,b)) * (h2 [x] (id- a)) & ( for h0 being Morphism of c,b |^ a st f2 = (eval (a,b)) * (h0 [x] (id- a)) holds
h2 = h0 ) ) by A14, A7;
assume L . x1 = L . x2 ; :: thesis: x1 = x2
hence x1 = x2 by A13, A15; :: thesis: verum

end;

then A16: L is one-to-one by A8, FUNCT_2:19;
for y being object st y in Hom (c,(b |^ a)) holds
y in rng L

proof

let y be object ; :: thesis: ( y in Hom (c,(b |^ a)) implies y in rng L )
assume y in Hom (c,(b |^ a)) ; :: thesis: y in rng L
then reconsider h = y as Morphism of c,b |^ a by CAT_7:def 3;
set f1 = (eval (a,b)) * (h [x] (id- a));
A17: (eval (a,b)) * (h [x] (id- a)) in Hom ((c [x] a),b) by A1, CAT_7:def 3;
then consider h1 being Morphism of c,b |^ a such that
A18: ( h1 = L . ((eval (a,b)) * (h [x] (id- a))) & (eval (a,b)) * (h [x] (id- a)) = (eval (a,b)) * (h1 [x] (id- a)) & ( for h0 being Morphism of c,b |^ a st (eval (a,b)) * (h [x] (id- a)) = (eval (a,b)) * (h0 [x] (id- a)) holds
h1 = h0 ) ) by A7;
A19: y = L . ((eval (a,b)) * (h [x] (id- a))) by A18;
(eval (a,b)) * (h [x] (id- a)) in dom L by A8, A17, FUNCT_2:def 1;
hence y in rng L by A19, FUNCT_1:3; :: thesis: verum

end;

then Hom (c,(b |^ a)) c= rng L by TARSKI:def 3;
then L is onto by FUNCT_2:def 3, XBOOLE_0:def 10;
hence L is bijective by A16; :: thesis: verum