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 ) )

A2: now :: thesis: ( A1 is Subset of A2 implies f1 union f2 = f2 )

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:65;
hence f1 union f2 = f2 by FUNCT_2:17; :: thesis: verum

end;

now :: thesis: ( f1 union f2 = f2 implies A1 is Subset of A2 )

A3: ( dom (f1 union f2) = A1 \/ A2 & dom f2 = A2 ) by FUNCT_2:def 1;
assume f1 union f2 = f2 ; :: thesis: A1 is Subset of A2
hence A1 is Subset of A2 by A3, XBOOLE_1:7; :: thesis: verum

end;

hence ( A1 is Subset of A2 iff f1 union f2 = f2 ) by A2; :: thesis: ( A2 is Subset of A1 iff f1 union f2 = f1 )

A4: now :: thesis: ( A2 is Subset of A1 implies f1 union f2 = f1 )

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:65;
hence f1 union f2 = f1 by FUNCT_2:17; :: thesis: verum

end;

now :: thesis: ( f1 union f2 = f1 implies A2 is Subset of A1 )

A5: ( dom (f1 union f2) = A1 \/ A2 & dom f1 = A1 ) by FUNCT_2:def 1;
assume f1 union f2 = f1 ; :: thesis: A2 is Subset of A1
hence A2 is Subset of A1 by A5, XBOOLE_1:7; :: thesis: verum

end;

hence ( A2 is Subset of A1 iff f1 union f2 = f1 ) by A4; :: thesis: verum