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)
( ( A1 = {} or A1 <> {} ) & ( A2 = {} or A2 <> {} ) ) ;
then A2: ( ( f = {} & ( A1 = {} or A2 = {} ) ) or ( dom f = A1 & A1 <> {} & A2 <> {} ) ) by Def1;
( ( B1 = {} or B1 <> {} ) & ( B2 = {} or B2 <> {} ) ) ;
then A3: ( ( g = {} & ( B1 = {} or B2 = {} ) ) or ( dom g = B1 & B1 <> {} & B2 <> {} ) ) by Def1;
A5: ( dom (f /\ g) c= (dom f) /\ (dom g) & rng (f /\ g) c= (rng f) /\ (rng g) & (dom f) /\ (dom g) c= A1 /\ B1 & (rng f) /\ (rng g) c= A2 /\ B2 ) by RELAT_1:14, RELAT_1:27, XBOOLE_1:27;
then A6: ( dom (f /\ g) c= A1 /\ B1 & rng (f /\ g) c= A2 /\ B2 ) by XBOOLE_1:1;
then A7: f /\ g is PartFunc of (A1 /\ B1),(A2 /\ B2) by RELSET_1:11;

A8: now

assume A9: ( dom f = A1 & A1 <> {} & dom g = B1 & B1 <> {} ) ; :: thesis: ( ( A1 /\ B1 <> {} implies A2 /\ B2 <> {} ) & dom (f /\ g) = A1 /\ B1 )
consider a being Element of A1 /\ B1;

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

assume A1 /\ B1 <> {} ; :: thesis: A2 /\ B2 <> {}
then ( f . a = g . a & a in A1 & a in B1 ) by A1, A9, PARTFUN1:def 6, XBOOLE_0:def 4;
then ( f . a in rng f & f . a in rng g ) by A9, FUNCT_1:def 5;
hence A2 /\ B2 <> {} by XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

thus dom (f /\ g) c= A1 /\ B1 by A5, 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 a in A1 /\ B1 ; :: thesis: a in dom (f /\ g)
then ( f . a = g . a & a in A1 & a in B1 ) by A1, A9, PARTFUN1:def 6, XBOOLE_0:def 4;
then ( [a,(f . a)] in f & [a,(f . a)] in g ) by A9, FUNCT_1:def 4;
then [a,(f . a)] in f /\ g by XBOOLE_0:def 4;
hence a in dom (f /\ g) by RELAT_1:def 4; :: thesis: verum

end;

end;

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 A2, A3, A8; :: thesis: verum

end;

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

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

end;

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

hence f /\ g = {} by A2, A3, A8; :: thesis: verum

end;

end;

end;

hence f /\ g is Function of (A1 /\ B1),(A2 /\ B2) by A6, Def1, RELSET_1:11; :: thesis: verum