let X be set ; :: thesis: for Y being RelStr holds Funcs (X, the carrier of Y) = the carrier of (Y |^ X)
let Y be RelStr ; :: thesis: Funcs (X, the carrier of Y) = the carrier of (Y |^ X)
set YY = the carrier of Y;
set f = Carrier (X --> Y);
A1: dom (Carrier (X --> Y)) = X by PARTFUN1:def 2;
A2: for x being set st x in X holds
(Carrier (X --> Y)) . x = the carrier of Y

proof

let x be set ; :: thesis: ( x in X implies (Carrier (X --> Y)) . x = the carrier of Y )
assume A3: x in X ; :: thesis: (Carrier (X --> Y)) . x = the carrier of Y
then ex R being 1-sorted st
( R = (X --> Y) . x & (Carrier (X --> Y)) . x = the carrier of R ) by PRALG_1:def 15;
hence (Carrier (X --> Y)) . x = the carrier of Y by A3, FUNCOP_1:7; :: thesis: verum

end;

Funcs (X, the carrier of Y) = product (Carrier (X --> Y))

proof

thus Funcs (X, the carrier of Y) c= product (Carrier (X --> Y)) :: according to XBOOLE_0:def 10 :: thesis: product (Carrier (X --> Y)) c= Funcs (X, the carrier of Y)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs (X, the carrier of Y) or x in product (Carrier (X --> Y)) )
assume x in Funcs (X, the carrier of Y) ; :: thesis: x in product (Carrier (X --> Y))
then consider g being Function such that
A4: x = g and
A5: dom g = X and
A6: rng g c= the carrier of Y by FUNCT_2:def 2;

now :: thesis: for y being object st y in dom (Carrier (X --> Y)) holds
g . y in (Carrier (X --> Y)) . y

let y be object ; :: thesis: ( y in dom (Carrier (X --> Y)) implies g . y in (Carrier (X --> Y)) . y )
assume y in dom (Carrier (X --> Y)) ; :: thesis: g . y in (Carrier (X --> Y)) . y
then ( (Carrier (X --> Y)) . y = the carrier of Y & g . y in rng g ) by A2, A5, FUNCT_1:def 3;
hence g . y in (Carrier (X --> Y)) . y by A6; :: thesis: verum

end;

hence x in product (Carrier (X --> Y)) by A1, A4, A5, CARD_3:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in product (Carrier (X --> Y)) or x in Funcs (X, the carrier of Y) )
assume x in product (Carrier (X --> Y)) ; :: thesis: x in Funcs (X, the carrier of Y)
then consider g being Function such that
A7: x = g and
A8: dom g = dom (Carrier (X --> Y)) and
A9: for x being object st x in dom (Carrier (X --> Y)) holds
g . x in (Carrier (X --> Y)) . x by CARD_3:def 5;
rng g c= the carrier of Y

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in the carrier of Y )
assume y in rng g ; :: thesis: y in the carrier of Y
then consider z being object such that
A10: z in dom g and
A11: y = g . z by FUNCT_1:def 3;
(Carrier (X --> Y)) . z = the carrier of Y by A2, A8, A10;
hence y in the carrier of Y by A8, A9, A10, A11; :: thesis: verum

end;

hence x in Funcs (X, the carrier of Y) by A1, A7, A8, FUNCT_2:def 2; :: thesis: verum

end;

hence Funcs (X, the carrier of Y) = the carrier of (Y |^ X) by Def4; :: thesis: verum