let A, B, C be set ; :: thesis: (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

let f be set ; :: thesis: ( f in (Funcs (A,B)) /\ (Funcs (A,C)) implies f in Funcs (A,(B /\ C)) )
assume f in (Funcs (A,B)) /\ (Funcs (A,C)) ; :: thesis: f in Funcs (A,(B /\ C))
then C0: ( f in Funcs (A,B) & f in Funcs (A,C) ) by XBOOLE_0:def 4;
consider f1 being Function such that
C1: ( f1 = f & dom f1 = A & rng f1 c= B ) by C0, FUNCT_2:def 2;
consider f2 being Function such that
C2: ( f2 = f & dom f2 = A & rng f2 c= C ) by C0, FUNCT_2:def 2;
( f1 = f & dom f1 = A & rng f1 c= B /\ C ) by C1, C2, XBOOLE_1:19;
hence f in Funcs (A,(B /\ C)) by FUNCT_2:def 2; :: thesis: verum

end;

then A1: (Funcs (A,B)) /\ (Funcs (A,C)) c= Funcs (A,(B /\ C)) by TARSKI:def 3;
( Funcs (A,(B /\ C)) c= Funcs (A,B) & Funcs (A,(B /\ C)) c= Funcs (A,C) ) by FUNCT_5:56, XBOOLE_1:17;
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 A1, XBOOLE_0:def 10; :: thesis: verum