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
f1 union f2 = f2 union f1
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
f1 union f2 = f2 union f1
let f1 be Function of A1,B; :: thesis: for f2 being Function of A2,B st f1 | (A1 /\ A2) = f2 | (A1 /\ A2) holds
f1 union f2 = f2 union f1
let f2 be Function of A2,B; :: thesis: ( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) implies f1 union f2 = f2 union f1 )
assume f1 | (A1 /\ A2) = f2 | (A1 /\ A2) ; :: thesis: f1 union f2 = f2 union f1
then ( (f1 union f2) | A1 = f1 & (f1 union f2) | A2 = f2 ) by Def1;
hence f1 union f2 = f2 union f1 by Th2; :: thesis: verum