let A, B, C be set ; (Funcs (A,B)) /\ (Funcs (A,C)) = Funcs (A,(B /\ C))
set L = (Funcs (A,B)) /\ (Funcs (A,C));
set R = Funcs (A,(B /\ C));
now for f being object st f in (Funcs (A,B)) /\ (Funcs (A,C)) holds
f in Funcs (A,(B /\ C))let f be
object ;
( f in (Funcs (A,B)) /\ (Funcs (A,C)) implies f in Funcs (A,(B /\ C)) )assume
f in (Funcs (A,B)) /\ (Funcs (A,C))
;
f in Funcs (A,(B /\ C))then A1:
(
f in Funcs (
A,
B) &
f in Funcs (
A,
C) )
by XBOOLE_0:def 4;
consider f1 being
Function such that A2:
(
f1 = f &
dom f1 = A &
rng f1 c= B )
by FUNCT_2:def 2, A1;
consider f2 being
Function such that A3:
(
f2 = f &
dom f2 = A &
rng f2 c= C )
by FUNCT_2:def 2, A1;
(
f1 = f &
dom f1 = A &
rng f1 c= B /\ C )
by XBOOLE_1:19, A2, A3;
hence
f in Funcs (
A,
(B /\ C))
by FUNCT_2:def 2;
verum end;
then A4:
(Funcs (A,B)) /\ (Funcs (A,C)) c= Funcs (A,(B /\ C))
;
( Funcs (A,(B /\ C)) c= Funcs (A,B) & Funcs (A,(B /\ C)) c= Funcs (A,C) )
by XBOOLE_1:17, FUNCT_5:56;
then
Funcs (A,(B /\ C)) c= (Funcs (A,B)) /\ (Funcs (A,C))
by XBOOLE_1:19;
hence
(Funcs (A,B)) /\ (Funcs (A,C)) = Funcs (A,(B /\ C))
by A4; verum