let A, B be non empty set ; :: thesis: 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
let A1, A2, A3 be non empty Subset of A; :: thesis: for 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
let A12, A23 be non empty Subset of A; :: thesis: ( A12 = A1 \/ A2 & A23 = A2 \/ A3 implies 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 )
assume A1: ( A12 = A1 \/ A2 & A23 = A2 \/ A3 ) ; :: thesis: 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
let f1 be Function of A1,B; :: thesis: 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
let f2 be Function of A2,B; :: thesis: 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
let f3 be Function of A3,B; :: thesis: ( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) implies 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 )
assume A2: ( f1 | (A1 /\ A2) = f2 | (A1 /\ A2) & f2 | (A2 /\ A3) = f3 | (A2 /\ A3) & f1 | (A1 /\ A3) = f3 | (A1 /\ A3) ) ; :: thesis: 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
let f12 be Function of A12,B; :: thesis: for f23 being Function of A23,B st f12 = f1 union f2 & f23 = f2 union f3 holds
f12 union f3 = f1 union f23
let f23 be Function of A23,B; :: thesis: ( f12 = f1 union f2 & f23 = f2 union f3 implies f12 union f3 = f1 union f23 )
assume A3: ( f12 = f1 union f2 & f23 = f2 union f3 ) ; :: thesis: f12 union f3 = f1 union f23
A1 \/ A23 = A12 \/ A3 by A1, XBOOLE_1:4;
then reconsider f = f12 union f3 as Function of (A1 \/ A23),B ;
A4: ( f12 | A1 = f1 & f12 | A2 = f2 ) by A2, A3, Def1;
A5: ( (f12 | A1) | (A1 /\ A3) = f1 | (A1 /\ A3) & (f12 | A2) | (A2 /\ A3) = f2 | (A2 /\ A3) & A1 /\ A3 c= A1 & A2 /\ A3 c= A2 ) by A2, A3, Def1, XBOOLE_1:17;
A12 /\ A3 c= A12 by XBOOLE_1:17;
then reconsider F = f12 | (A12 /\ A3) as Function of (A12 /\ A3),B by FUNCT_2:38;
A12 /\ A3 c= A3 by XBOOLE_1:17;
then reconsider G = f3 | (A12 /\ A3) as Function of (A12 /\ A3),B by FUNCT_2:38;

now

let x be set ; :: thesis: ( x in A12 /\ A3 implies F . x = G . x )
assume A6: x in A12 /\ A3 ; :: thesis: F . x = G . x
A7: A12 /\ A3 = (A1 /\ A3) \/ (A2 /\ A3) by A1, XBOOLE_1:23;
A8: ( A1 /\ A3 c= A12 /\ A3 & A2 /\ A3 c= A12 /\ A3 ) by A1, XBOOLE_1:7, XBOOLE_1:26;

A9: now

assume A10: x in A1 /\ A3 ; :: thesis: F . x = G . x
hence F . x = (F | (A1 /\ A3)) . x by FUNCT_1:72
.= (f12 | (A1 /\ A3)) . x by A8, FUNCT_1:82
.= (f3 | (A1 /\ A3)) . x by A2, A5, FUNCT_1:82
.= (G | (A1 /\ A3)) . x by A8, FUNCT_1:82
.= G . x by A10, FUNCT_1:72 ;
:: thesis: verum

end;

now

assume A11: x in A2 /\ A3 ; :: thesis: F . x = G . x
hence F . x = (F | (A2 /\ A3)) . x by FUNCT_1:72
.= (f12 | (A2 /\ A3)) . x by A8, FUNCT_1:82
.= (f3 | (A2 /\ A3)) . x by A2, A5, FUNCT_1:82
.= (G | (A2 /\ A3)) . x by A8, FUNCT_1:82
.= G . x by A11, FUNCT_1:72 ;
:: thesis: verum

end;

hence F . x = G . x by A6, A7, A9, XBOOLE_0:def 3; :: thesis: verum

end;

then A12: f12 | (A12 /\ A3) = f3 | (A12 /\ A3) by FUNCT_2:18;
then ( (f | A12) | A1 = f12 | A1 & (f | A12) | A2 = f12 | A2 & A1 c= A12 & A2 c= A12 ) by A1, Def1, XBOOLE_1:7;
then A13: ( f | A1 = f1 & f | A2 = f2 ) by A4, FUNCT_1:82;
A23 c= A1 \/ A23 by XBOOLE_1:7;
then reconsider H = f | A23 as Function of A23,B by FUNCT_2:38;

now

let x be set ; :: thesis: ( x in A23 implies H . x = f23 . x )
assume A14: x in A23 ; :: thesis: H . x = f23 . x

A15: now

assume A16: x in A2 ; :: thesis: H . x = f23 . x
thus H . x = f . x by A14, FUNCT_1:72
.= f2 . x by A13, A16, FUNCT_1:72
.= (f23 | A2) . x by A2, A3, Def1
.= f23 . x by A16, FUNCT_1:72 ; :: thesis: verum

end;

now

assume A17: x in A3 ; :: thesis: H . x = f23 . x
thus H . x = f . x by A14, FUNCT_1:72
.= (f | A3) . x by A17, FUNCT_1:72
.= f3 . x by A12, Def1
.= (f23 | A3) . x by A2, A3, Def1
.= f23 . x by A17, FUNCT_1:72 ; :: thesis: verum

end;

hence H . x = f23 . x by A1, A14, A15, XBOOLE_0:def 3; :: thesis: verum

end;

then f | A23 = f23 by FUNCT_2:18;
hence f12 union f3 = f1 union f23 by A13, Th7; :: thesis: verum