let A1, A2, B1, B2 be set ; :: thesis: for f being Function of A1,A2
for g being Function of B1,B2 st f tolerates g holds
f /\ g is Function of (A1 /\ B1),(A2 /\ B2)
let f be Function of A1,A2; :: thesis: for g being Function of B1,B2 st f tolerates g holds
f /\ g is Function of (A1 /\ B1),(A2 /\ B2)
let g be Function of B1,B2; :: thesis: ( f tolerates g implies f /\ g is Function of (A1 /\ B1),(A2 /\ B2) )
assume A1: f tolerates g ; :: thesis: f /\ g is Function of (A1 /\ B1),(A2 /\ B2)
A2: ( dom (f /\ g) c= (dom f) /\ (dom g) & (dom f) /\ (dom g) c= A1 /\ B1 ) by RELAT_1:2, XBOOLE_1:27;

A3: now

set a = the Element of A1 /\ B1;
assume that
A4: dom f = A1 and
A1 <> {} and
A5: dom g = B1 and
B1 <> {} ; :: thesis: ( ( A1 /\ B1 <> {} implies A2 /\ B2 <> {} ) & dom (f /\ g) = A1 /\ B1 )

hereby :: thesis: dom (f /\ g) = A1 /\ B1

assume A6: A1 /\ B1 <> {} ; :: thesis: A2 /\ B2 <> {}
then the Element of A1 /\ B1 in A1 by XBOOLE_0:def 4;
then A7: f . the Element of A1 /\ B1 in rng f by A4, FUNCT_1:def 3;
( f . the Element of A1 /\ B1 = g . the Element of A1 /\ B1 & the Element of A1 /\ B1 in B1 ) by A1, A4, A5, A6, PARTFUN1:def 4, XBOOLE_0:def 4;
then f . the Element of A1 /\ B1 in rng g by A5, FUNCT_1:def 3;
hence A2 /\ B2 <> {} by A7, XBOOLE_0:def 4; :: thesis: verum

end;

thus dom (f /\ g) = A1 /\ B1 :: thesis: verum

proof

thus dom (f /\ g) c= A1 /\ B1 by A2, XBOOLE_1:1; :: according to XBOOLE_0:def 10 :: thesis: A1 /\ B1 c= dom (f /\ g)
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A1 /\ B1 or a in dom (f /\ g) )
assume A8: a in A1 /\ B1 ; :: thesis: a in dom (f /\ g)
then a in A1 by XBOOLE_0:def 4;
then A9: [a,(f . a)] in f by A4, FUNCT_1:def 2;
( f . a = g . a & a in B1 ) by A1, A4, A5, A8, PARTFUN1:def 4, XBOOLE_0:def 4;
then [a,(f . a)] in g by A5, FUNCT_1:def 2;
then [a,(f . a)] in f /\ g by A9, XBOOLE_0:def 4;
hence a in dom (f /\ g) by RELAT_1:def 4; :: thesis: verum

end;

end;

( rng (f /\ g) c= (rng f) /\ (rng g) & (rng f) /\ (rng g) c= A2 /\ B2 ) by RELAT_1:13, XBOOLE_1:27;
then A10: rng (f /\ g) c= A2 /\ B2 by XBOOLE_1:1;
( A2 = {} or A2 <> {} ) ;
then A11: ( ( f = {} & ( A1 = {} or A2 = {} ) ) or ( dom f = A1 & A1 <> {} & A2 <> {} ) ) by Def1;
A12: ( B2 = {} or B2 <> {} ) ;

A13: now

per cases ( A2 /\ B2 <> {} or A1 /\ B1 = {} or ( A2 /\ B2 = {} & A1 /\ B1 <> {} ) ) ;

case A2 /\ B2 <> {} ; :: thesis: dom (f /\ g) = A1 /\ B1

hence dom (f /\ g) = A1 /\ B1 by A11, A12, A3, Def1; :: thesis: verum

end;

case A1 /\ B1 = {} ; :: thesis: dom (f /\ g) = A1 /\ B1

hence dom (f /\ g) = A1 /\ B1 by A2; :: thesis: verum

end;

case ( A2 /\ B2 = {} & A1 /\ B1 <> {} ) ; :: thesis: f /\ g = {}

hence f /\ g = {} by A11, A12, A3, Def1; :: thesis: verum

end;

end;

end;

dom (f /\ g) c= A1 /\ B1 by A2, XBOOLE_1:1;
hence f /\ g is Function of (A1 /\ B1),(A2 /\ B2) by A10, A13, Def1, RELSET_1:4; :: thesis: verum