let A, B be non empty set ; :: thesis: for A1, A2 being non empty Subset of A
for f1 being Function of A1,B
for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds
( ( A1 is Subset of A2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies A1 is Subset of A2 ) & ( A2 is Subset of A1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies A2 is Subset of A1 ) )
let A1, A2 be non empty Subset of A; :: thesis: for f1 being Function of A1,B
for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds
( ( A1 is Subset of A2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies A1 is Subset of A2 ) & ( A2 is Subset of A1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies A2 is Subset of A1 ) )
let f1 be Function of A1,B; :: thesis: for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds
( ( A1 is Subset of A2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies A1 is Subset of A2 ) & ( A2 is Subset of A1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies A2 is Subset of A1 ) )
let f2 be Function of A2,B; :: thesis: ( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) implies ( ( A1 is Subset of A2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies A1 is Subset of A2 ) & ( A2 is Subset of A1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies A2 is Subset of A1 ) ) )
assume A1: f1 | (A1 /\ A2) = f2 | (A1 /\ A2) ; :: thesis: ( ( A1 is Subset of A2 implies f1 union f2 = f2 ) & ( f1 union f2 = f2 implies A1 is Subset of A2 ) & ( A2 is Subset of A1 implies f1 union f2 = f1 ) & ( f1 union f2 = f1 implies A2 is Subset of A1 ) )
thus ( A1 is Subset of A2 iff f1 union f2 = f2 ) :: thesis: ( A2 is Subset of A1 iff f1 union f2 = f1 )
proof
A2: now
assume A1 is Subset of A2 ; :: thesis: f1 union f2 = f2
then A2 = A1 \/ A2 by XBOOLE_1:12;
then (f1 union f2) | (A1 \/ A2) = f2 by A1, Def1;
then (f1 union f2) * (id (A1 \/ A2)) = f2 by RELAT_1:94;
hence f1 union f2 = f2 by FUNCT_2:23; :: thesis: verum
end;
now
assume f1 union f2 = f2 ; :: thesis: A1 is Subset of A2
then ( dom (f1 union f2) = dom f2 & dom (f1 union f2) = A1 \/ A2 & dom f2 = A2 ) by FUNCT_2:def 1;
hence A1 is Subset of A2 by XBOOLE_1:7; :: thesis: verum
end;
hence ( A1 is Subset of A2 iff f1 union f2 = f2 ) by A2; :: thesis: verum
end;
thus ( A2 is Subset of A1 iff f1 union f2 = f1 ) :: thesis: verum
proof
A3: now
assume A2 is Subset of A1 ; :: thesis: f1 union f2 = f1
then A1 = A1 \/ A2 by XBOOLE_1:12;
then (f1 union f2) | (A1 \/ A2) = f1 by A1, Def1;
then (f1 union f2) * (id (A1 \/ A2)) = f1 by RELAT_1:94;
hence f1 union f2 = f1 by FUNCT_2:23; :: thesis: verum
end;
now
assume f1 union f2 = f1 ; :: thesis: A2 is Subset of A1
then ( dom (f1 union f2) = dom f1 & dom (f1 union f2) = A1 \/ A2 & dom f1 = A1 ) by FUNCT_2:def 1;
hence A2 is Subset of A1 by XBOOLE_1:7; :: thesis: verum
end;
hence ( A2 is Subset of A1 iff f1 union f2 = f1 ) by A3; :: thesis: verum
end;