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 that
A1: A12 = A1 \/ A2 and
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 that
A3: f1 | (A1 /\ A2) = f2 | (A1 /\ A2) and
A4: f2 | (A2 /\ A3) = f3 | (A2 /\ A3) and
A5: 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 that
A6: f12 = f1 union f2 and
A7: f23 = f2 union f3 ; :: thesis: f12 union f3 = f1 union f23
A8: (f12 | A2) | (A2 /\ A3) = f2 | (A2 /\ A3) by A3, A6, Def1;
A1 \/ A23 = A12 \/ A3 by A1, A2, XBOOLE_1:4;
then reconsider f = f12 union f3 as Function of (A1 \/ A23),B ;
A12 /\ A3 c= A12 by XBOOLE_1:17;
then reconsider F = f12 | (A12 /\ A3) as Function of (A12 /\ A3),B by FUNCT_2:32;
A9: A2 /\ A3 c= A2 by XBOOLE_1:17;
A10: f12 | A2 = f2 by A3, A6, Def1;
A23 c= A1 \/ A23 by XBOOLE_1:7;
then reconsider H = f | A23 as Function of A23,B by FUNCT_2:32;
A11: A2 c= A12 by A1, XBOOLE_1:7;
A12 /\ A3 c= A3 by XBOOLE_1:17;
then reconsider G = f3 | (A12 /\ A3) as Function of (A12 /\ A3),B by FUNCT_2:32;
A12: A1 /\ A3 c= A1 by XBOOLE_1:17;
A13: (f12 | A1) | (A1 /\ A3) = f1 | (A1 /\ A3) by A3, A6, Def1;
now :: thesis: for x being object st x in A12 /\ A3 holds
F . x = G . x
let x be object ; :: thesis: ( x in A12 /\ A3 implies F . x = G . x )
assume A14: x in A12 /\ A3 ; :: thesis: F . x = G . x
A15: A1 /\ A3 c= A12 /\ A3 by A1, XBOOLE_1:7, XBOOLE_1:26;
A16: now :: thesis: ( x in A1 /\ A3 implies F . x = G . x )
assume A17: x in A1 /\ A3 ; :: thesis: F . x = G . x
hence F . x = (F | (A1 /\ A3)) . x by FUNCT_1:49
.= (f12 | (A1 /\ A3)) . x by A15, FUNCT_1:51
.= (f3 | (A1 /\ A3)) . x by A5, A13, A12, FUNCT_1:51
.= (G | (A1 /\ A3)) . x by A15, FUNCT_1:51
.= G . x by A17, FUNCT_1:49 ;
:: thesis: verum
end;
A18: A2 /\ A3 c= A12 /\ A3 by A1, XBOOLE_1:7, XBOOLE_1:26;
A19: now :: thesis: ( x in A2 /\ A3 implies F . x = G . x )
assume A20: x in A2 /\ A3 ; :: thesis: F . x = G . x
hence F . x = (F | (A2 /\ A3)) . x by FUNCT_1:49
.= (f12 | (A2 /\ A3)) . x by A18, FUNCT_1:51
.= (f3 | (A2 /\ A3)) . x by A4, A8, A9, FUNCT_1:51
.= (G | (A2 /\ A3)) . x by A18, FUNCT_1:51
.= G . x by A20, FUNCT_1:49 ;
:: thesis: verum
end;
A12 /\ A3 = (A1 /\ A3) \/ (A2 /\ A3) by A1, XBOOLE_1:23;
hence F . x = G . x by A14, A16, A19, XBOOLE_0:def 3; :: thesis: verum
end;
then A21: f12 | (A12 /\ A3) = f3 | (A12 /\ A3) by FUNCT_2:12;
then A22: (f | A12) | A1 = f12 | A1 by Def1;
(f | A12) | A2 = f12 | A2 by A21, Def1;
then A23: f | A2 = f2 by A10, A11, FUNCT_1:51;
now :: thesis: for x being object st x in A23 holds
H . x = f23 . x
let x be object ; :: thesis: ( x in A23 implies H . x = f23 . x )
assume A24: x in A23 ; :: thesis: H . x = f23 . x
A25: now :: thesis: ( x in A2 implies H . x = f23 . x )
assume A26: x in A2 ; :: thesis: H . x = f23 . x
thus H . x = f . x by A24, FUNCT_1:49
.= f2 . x by A23, A26, FUNCT_1:49
.= (f23 | A2) . x by A4, A7, Def1
.= f23 . x by A26, FUNCT_1:49 ; :: thesis: verum
end;
now :: thesis: ( x in A3 implies H . x = f23 . x )
assume A27: x in A3 ; :: thesis: H . x = f23 . x
thus H . x = f . x by A24, FUNCT_1:49
.= (f | A3) . x by A27, FUNCT_1:49
.= f3 . x by A21, Def1
.= (f23 | A3) . x by A4, A7, Def1
.= f23 . x by A27, FUNCT_1:49 ; :: thesis: verum
end;
hence H . x = f23 . x by A2, A24, A25, XBOOLE_0:def 3; :: thesis: verum
end;
then A28: f | A23 = f23 by FUNCT_2:12;
A29: A1 c= A12 by A1, XBOOLE_1:7;
f12 | A1 = f1 by A3, A6, Def1;
then f | A1 = f1 by A22, A29, FUNCT_1:51;
hence f12 union f3 = f1 union f23 by A28, Th2; :: thesis: verum