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 XBOOLE_1:27, XTUPLE_0:24;
A3: now :: thesis: ( dom f = A1 & A1 <> {} & dom g = B1 & B1 <> {} implies ( ( A1 /\ B1 <> {} implies A2 /\ B2 <> {} ) & dom (f /\ g) = A1 /\ B1 ) )
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, 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; :: according to XBOOLE_0:def 10 :: thesis: A1 /\ B1 c= dom (f /\ g)
let a be object ; :: 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, 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 XTUPLE_0:def 12; :: 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 ;
A11: ( A2 = {} or A2 <> {} ) ;
A12: ( B2 = {} or B2 <> {} ) ;
A13: now :: thesis: ( ( A2 /\ B2 <> {} & dom (f /\ g) = A1 /\ B1 ) or ( A1 /\ B1 = {} & dom (f /\ g) = A1 /\ B1 ) or ( A2 /\ B2 = {} & A1 /\ B1 <> {} & f /\ g = {} ) )
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 A12, A3, Def1, A11; :: 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 A12, A3, Def1, A11; :: thesis: verum
end;
end;
end;
thus f /\ g is Function of (A1 /\ B1),(A2 /\ B2) by A10, A13, Def1, RELSET_1:4; :: thesis: verum