theorem
for
A,
B being non
empty set for
A1,
A2,
A3,
A12,
A23 being non
empty Subset of
A st
A12 = A1 \/ A2 &
A23 = A2 \/ A3 holds
for
f1 being
Function of
A1,
B for
f2 being
Function of
A2,
B for
f3 being
Function of
A3,
B st
f1 | (A1 /\ A2) = f2 | (A1 /\ A2) &
f2 | (A2 /\ A3) = f3 | (A2 /\ A3) &
f1 | (A1 /\ A3) = f3 | (A1 /\ A3) holds
for
f12 being
Function of
A12,
B for
f23 being
Function of
A23,
B st
f12 = f1 union f2 &
f23 = f2 union f3 holds
f12 union f3 = f1 union f23
Lm1:
for A being set holds {} is Function of A,{}