let Y be non empty set ; :: thesis: for A, B, C, D being a_partition of Y
for h being Function
for A9, B9, C9, D9 being object st A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
( h . B = B9 & h . C = C9 & h . D = D9 )
let A, B, C, D be a_partition of Y; :: thesis: for h being Function
for A9, B9, C9, D9 being object st A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
( h . B = B9 & h . C = C9 & h . D = D9 )
let h be Function; :: thesis: for A9, B9, C9, D9 being object st A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) holds
( h . B = B9 & h . C = C9 & h . D = D9 )
let A9, B9, C9, D9 be object ; :: thesis: ( A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & h = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) implies ( h . B = B9 & h . C = C9 & h . D = D9 ) )
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 .--> B9) +* (C .--> C9)) +* (D .--> D9)) +* (A .--> A9) ; :: thesis: ( h . B = B9 & h . C = C9 & h . D = D9 )
not D in dom (A .--> A9) by A3, TARSKI:def 1;
then A9: h . D = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . D by A7, FUNCT_4:11;
not C in dom (A .--> A9) by A2, TARSKI:def 1;
then A10: h . C = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . C by A7, FUNCT_4:11;
not C in dom (D .--> D9) by A6, TARSKI:def 1;
then A12: h . C = ((B .--> B9) +* (C .--> C9)) . C by A10, FUNCT_4:11;
not B in dom (A .--> A9) by A1, TARSKI:def 1;
then A13: h . B = (((B .--> B9) +* (C .--> C9)) +* (D .--> D9)) . B by A7, FUNCT_4:11;
not B in dom (D .--> D9) by A5, TARSKI:def 1;
then A14: h . B = ((B .--> B9) +* (C .--> C9)) . B by A13, FUNCT_4:11;
not B in dom (C .--> C9) by A4, TARSKI:def 1;
then h . B = (B .--> B9) . B by A14, FUNCT_4:11;
hence h . B = B9 by FUNCOP_1:72; :: thesis: ( h . C = C9 & h . D = D9 )
C in dom (C .--> C9) by TARSKI:def 1;
then h . C = (C .--> C9) . C by A12, FUNCT_4:13;
hence h . C = C9 by FUNCOP_1:72; :: thesis: h . D = D9
D in dom (D .--> D9) by TARSKI:def 1;
then h . D = (D .--> D9) . D by A9, FUNCT_4:13;
hence h . D = D9 by FUNCOP_1:72; :: thesis: verum