let f1, f2, g1, g2 be Function; :: thesis: [:f1,f2:] /\ [:g1,g2:] = [:(f1 /\ g1),(f2 /\ g2):]
set H1 = f1 /\ g1;
set H2 = f2 /\ g2;
set F = [:f1,f2:];
set G = [:g1,g2:];
set lh = [:f1,f2:] /\ [:g1,g2:];
reconsider H1 = f1 /\ g1, H2 = f2 /\ g2 as Function ;
set rh = [:H1,H2:];

now :: thesis: for x being set st x in ([:f1,f2:] /\ [:g1,g2:]) \/ [:H1,H2:] holds
( x in [:f1,f2:] /\ [:g1,g2:] iff x in [:H1,H2:] )

let x be set ; :: thesis: ( x in ([:f1,f2:] /\ [:g1,g2:]) \/ [:H1,H2:] implies ( x in [:f1,f2:] /\ [:g1,g2:] iff x in [:H1,H2:] ) )
set y = x `1 ;
set z = x `2 ;
set x1 = (x `1) `1 ;
set x2 = (x `1) `2 ;
set x3 = (x `2) `1 ;
set x4 = (x `2) `2 ;
set xx = [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]];
( [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:f1,f2:] /\ [:g1,g2:] iff ( [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:f1,f2:] & [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:g1,g2:] ) ) by XBOOLE_0:def 4;
then ( [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:f1,f2:] /\ [:g1,g2:] iff ( [((x `1) `1),((x `2) `1)] in f1 & [((x `1) `1),((x `2) `1)] in g1 & [((x `1) `2),((x `2) `2)] in f2 & [((x `1) `2),((x `2) `2)] in g2 ) ) by Lm73;
then ( [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:f1,f2:] /\ [:g1,g2:] iff ( [((x `1) `1),((x `2) `1)] in f1 /\ g1 & [((x `1) `2),((x `2) `2)] in f2 /\ g2 ) ) by XBOOLE_0:def 4;
then A1: ( [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:f1,f2:] /\ [:g1,g2:] iff [[((x `1) `1),((x `1) `2)],[((x `2) `1),((x `2) `2)]] in [:H1,H2:] ) by Lm73;
assume x in ([:f1,f2:] /\ [:g1,g2:]) \/ [:H1,H2:] ; :: thesis: ( x in [:f1,f2:] /\ [:g1,g2:] iff x in [:H1,H2:] )
thus ( x in [:f1,f2:] /\ [:g1,g2:] iff x in [:H1,H2:] ) by A1, Lm75; :: thesis: verum

end;

hence [:f1,f2:] /\ [:g1,g2:] = [:(f1 /\ g1),(f2 /\ g2):] by Lm74; :: thesis: verum