let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y
for h being Function
for A', B', C', D' being set st G = {A,B,C,D} & 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 G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D being a_partition of Y
for h being Function
for A', B', C', D' being set st G = {A,B,C,D} & 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 G = {A,B,C,D} & 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 G = {A,B,C,D} & 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: ( G = {A,B,C,D} & 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 A1: ( G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') ) ; :: thesis: ( h . B = B' & h . C = C' & h . D = D' )
A2: dom (C .--> C') = {C} by FUNCOP_1:19;
A3: dom (D .--> D') = {D} by FUNCOP_1:19;
A4: dom (A .--> A') = {A} by FUNCOP_1:19;
thus h . B = B' :: thesis: ( h . C = C' & h . D = D' )

proof

not B in dom (A .--> A') by A1, A4, TARSKI:def 1;
then A5: h . B = (((B .--> B') +* (C .--> C')) +* (D .--> D')) . B by A1, FUNCT_4:12;
not B in dom (D .--> D') by A1, A3, TARSKI:def 1;
then A6: h . B = ((B .--> B') +* (C .--> C')) . B by A5, FUNCT_4:12;
not B in dom (C .--> C') by A1, A2, TARSKI:def 1;
then h . B = (B .--> B') . B by A6, FUNCT_4:12;
hence h . B = B' by FUNCOP_1:87; :: thesis: verum

end;

thus h . C = C' :: thesis: h . D = D'

proof

not C in dom (A .--> A') by A1, A4, TARSKI:def 1;
then A7: h . C = (((B .--> B') +* (C .--> C')) +* (D .--> D')) . C by A1, FUNCT_4:12;
not C in dom (D .--> D') by A1, A3, TARSKI:def 1;
then A8: h . C = ((B .--> B') +* (C .--> C')) . C by A7, FUNCT_4:12;
C in dom (C .--> C') by A2, TARSKI:def 1;
then h . C = (C .--> C') . C by A8, FUNCT_4:14;
hence h . C = C' by FUNCOP_1:87; :: thesis: verum

end;

not D in dom (A .--> A') by A1, A4, TARSKI:def 1;
then A9: h . D = (((B .--> B') +* (C .--> C')) +* (D .--> D')) . D by A1, FUNCT_4:12;
D in dom (D .--> D') by A3, TARSKI:def 1;
then h . D = (D .--> D') . D by A9, FUNCT_4:14;
hence h . D = D' by FUNCOP_1:87; :: thesis: verum