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);
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 A1: x in X ; :: thesis: (Carrier (X --> Y)) . x = the carrier of Y
then consider R being 1-sorted such that
A2: ( R = (X --> Y) . x & (Carrier (X --> Y)) . x = the carrier of R ) by PRALG_1:def 13;
thus (Carrier (X --> Y)) . x = the carrier of Y by A1, A2, FUNCOP_1:13; :: thesis: verum

end;

then A3: ( dom (Carrier (X --> Y)) = X & ( for x being set st x in X holds
(Carrier (X --> Y)) . x = the carrier of Y ) ) by PARTFUN1:def 4;
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 set ; :: 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 & dom g = X & rng g c= the carrier of Y ) by FUNCT_2:def 2;

now

let y be set ; :: 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 & the carrier of Y = the carrier of Y & g . y in rng g ) by A3, A4, FUNCT_1:def 5;
hence g . y in (Carrier (X --> Y)) . y by A4; :: thesis: verum

end;

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

end;

let x be set ; :: 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
A5: ( x = g & dom g = dom (Carrier (X --> Y)) & ( for x being set 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 set ; :: 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 set such that
A6: ( z in dom g & y = g . z ) by FUNCT_1:def 5;
( y in (Carrier (X --> Y)) . z & (Carrier (X --> Y)) . z = the carrier of Y & the carrier of Y = the carrier of Y ) by A3, A5, A6;
hence y in the carrier of Y ; :: thesis: verum

end;

hence x in Funcs X,the carrier of Y by A3, A5, FUNCT_2:def 2; :: thesis: verum

end;

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