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 :: thesis: for f being object st f in (Funcs (A,B)) /\ (Funcs (A,C)) holds
f in Funcs (A,(B /\ C))

let f be object ; :: 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 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; :: thesis: 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; :: thesis: verum