let Y be non empty set ; :: thesis: for A, B, C, D being a_partition of Y
for h being Function
for A', B', C', D' being set st A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
( h . B = B' & h . C = C' & h . D = D' )
let A, B, C, D be a_partition of Y; :: thesis: for h being Function
for A', B', C', D' being set st A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
( h . B = B' & h . C = C' & h . D = D' )
let h be Function; :: thesis: for A', B', C', D' being set st A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
( h . B = B' & h . C = C' & h . D = D' )
let A', B', C', D' be set ; :: thesis: ( A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') implies ( h . B = B' & h . C = C' & h . D = D' ) )
assume that
A1: A <> B and
A2: A <> C and
A3: A <> D and
A4: B <> C and
A5: B <> D and
A6: C <> D and
A7: h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') ; :: thesis: ( h . B = B' & h . C = C' & h . D = D' )
A8: dom (A .--> A') = {A} by FUNCOP_1:19;
then not D in dom (A .--> A') by A3, TARSKI:def 1;
then A9: h . D = (((B .--> B') +* (C .--> C')) +* (D .--> D')) . D by A7, FUNCT_4:12;
not C in dom (A .--> A') by A2, A8, TARSKI:def 1;
then A10: h . C = (((B .--> B') +* (C .--> C')) +* (D .--> D')) . C by A7, FUNCT_4:12;
A11: dom (D .--> D') = {D} by FUNCOP_1:19;
then not C in dom (D .--> D') by A6, TARSKI:def 1;
then A12: h . C = ((B .--> B') +* (C .--> C')) . C by A10, FUNCT_4:12;
not B in dom (A .--> A') by A1, A8, TARSKI:def 1;
then A13: h . B = (((B .--> B') +* (C .--> C')) +* (D .--> D')) . B by A7, FUNCT_4:12;
not B in dom (D .--> D') by A5, A11, TARSKI:def 1;
then A14: h . B = ((B .--> B') +* (C .--> C')) . B by A13, FUNCT_4:12;
A15: dom (C .--> C') = {C} by FUNCOP_1:19;
then not B in dom (C .--> C') by A4, TARSKI:def 1;
then h . B = (B .--> B') . B by A14, FUNCT_4:12;
hence h . B = B' by FUNCOP_1:87; :: thesis: ( h . C = C' & h . D = D' )
C in dom (C .--> C') by A15, TARSKI:def 1;
then h . C = (C .--> C') . C by A12, FUNCT_4:14;
hence h . C = C' by FUNCOP_1:87; :: thesis: h . D = D'
D in dom (D .--> D') by A11, TARSKI:def 1;
then h . D = (D .--> D') . D by A9, FUNCT_4:14;
hence h . D = D' by FUNCOP_1:87; :: thesis: verum