let x be Element of 64 -tuples_on BOOLEAN; :: thesis: DES-IPINV (DES-IP x) = x
set y = DES-IP x;
set z = DES-IPINV (DES-IP x);
( len x = 64 & len (DES-IPINV (DES-IP x)) = 64 ) by CARD_1:def 7;
then A1: ( dom x = Seg 64 & dom (DES-IPINV (DES-IP x)) = Seg 64 ) by FINSEQ_1:def 3;
A2: ( (DES-IPINV (DES-IP x)) . 1 = (DES-IP x) . 40 & (DES-IPINV (DES-IP x)) . 2 = (DES-IP x) . 8 & (DES-IPINV (DES-IP x)) . 3 = (DES-IP x) . 48 & (DES-IPINV (DES-IP x)) . 4 = (DES-IP x) . 16 & (DES-IPINV (DES-IP x)) . 5 = (DES-IP x) . 56 & (DES-IPINV (DES-IP x)) . 6 = (DES-IP x) . 24 & (DES-IPINV (DES-IP x)) . 7 = (DES-IP x) . 64 & (DES-IPINV (DES-IP x)) . 8 = (DES-IP x) . 32 & (DES-IPINV (DES-IP x)) . 9 = (DES-IP x) . 39 & (DES-IPINV (DES-IP x)) . 10 = (DES-IP x) . 7 & (DES-IPINV (DES-IP x)) . 11 = (DES-IP x) . 47 & (DES-IPINV (DES-IP x)) . 12 = (DES-IP x) . 15 & (DES-IPINV (DES-IP x)) . 13 = (DES-IP x) . 55 & (DES-IPINV (DES-IP x)) . 14 = (DES-IP x) . 23 & (DES-IPINV (DES-IP x)) . 15 = (DES-IP x) . 63 & (DES-IPINV (DES-IP x)) . 16 = (DES-IP x) . 31 & (DES-IPINV (DES-IP x)) . 17 = (DES-IP x) . 38 & (DES-IPINV (DES-IP x)) . 18 = (DES-IP x) . 6 & (DES-IPINV (DES-IP x)) . 19 = (DES-IP x) . 46 & (DES-IPINV (DES-IP x)) . 20 = (DES-IP x) . 14 & (DES-IPINV (DES-IP x)) . 21 = (DES-IP x) . 54 & (DES-IPINV (DES-IP x)) . 22 = (DES-IP x) . 22 & (DES-IPINV (DES-IP x)) . 23 = (DES-IP x) . 62 & (DES-IPINV (DES-IP x)) . 24 = (DES-IP x) . 30 & (DES-IPINV (DES-IP x)) . 25 = (DES-IP x) . 37 & (DES-IPINV (DES-IP x)) . 26 = (DES-IP x) . 5 & (DES-IPINV (DES-IP x)) . 27 = (DES-IP x) . 45 & (DES-IPINV (DES-IP x)) . 28 = (DES-IP x) . 13 & (DES-IPINV (DES-IP x)) . 29 = (DES-IP x) . 53 & (DES-IPINV (DES-IP x)) . 30 = (DES-IP x) . 21 & (DES-IPINV (DES-IP x)) . 31 = (DES-IP x) . 61 & (DES-IPINV (DES-IP x)) . 32 = (DES-IP x) . 29 & (DES-IPINV (DES-IP x)) . 33 = (DES-IP x) . 36 & (DES-IPINV (DES-IP x)) . 34 = (DES-IP x) . 4 & (DES-IPINV (DES-IP x)) . 35 = (DES-IP x) . 44 & (DES-IPINV (DES-IP x)) . 36 = (DES-IP x) . 12 & (DES-IPINV (DES-IP x)) . 37 = (DES-IP x) . 52 & (DES-IPINV (DES-IP x)) . 38 = (DES-IP x) . 20 & (DES-IPINV (DES-IP x)) . 39 = (DES-IP x) . 60 & (DES-IPINV (DES-IP x)) . 40 = (DES-IP x) . 28 & (DES-IPINV (DES-IP x)) . 41 = (DES-IP x) . 35 & (DES-IPINV (DES-IP x)) . 42 = (DES-IP x) . 3 & (DES-IPINV (DES-IP x)) . 43 = (DES-IP x) . 43 & (DES-IPINV (DES-IP x)) . 44 = (DES-IP x) . 11 & (DES-IPINV (DES-IP x)) . 45 = (DES-IP x) . 51 & (DES-IPINV (DES-IP x)) . 46 = (DES-IP x) . 19 & (DES-IPINV (DES-IP x)) . 47 = (DES-IP x) . 59 & (DES-IPINV (DES-IP x)) . 48 = (DES-IP x) . 27 & (DES-IPINV (DES-IP x)) . 49 = (DES-IP x) . 34 & (DES-IPINV (DES-IP x)) . 50 = (DES-IP x) . 2 & (DES-IPINV (DES-IP x)) . 51 = (DES-IP x) . 42 & (DES-IPINV (DES-IP x)) . 52 = (DES-IP x) . 10 & (DES-IPINV (DES-IP x)) . 53 = (DES-IP x) . 50 & (DES-IPINV (DES-IP x)) . 54 = (DES-IP x) . 18 & (DES-IPINV (DES-IP x)) . 55 = (DES-IP x) . 58 & (DES-IPINV (DES-IP x)) . 56 = (DES-IP x) . 26 & (DES-IPINV (DES-IP x)) . 57 = (DES-IP x) . 33 & (DES-IPINV (DES-IP x)) . 58 = (DES-IP x) . 1 & (DES-IPINV (DES-IP x)) . 59 = (DES-IP x) . 41 & (DES-IPINV (DES-IP x)) . 60 = (DES-IP x) . 9 & (DES-IPINV (DES-IP x)) . 61 = (DES-IP x) . 49 & (DES-IPINV (DES-IP x)) . 62 = (DES-IP x) . 17 & (DES-IPINV (DES-IP x)) . 63 = (DES-IP x) . 57 & (DES-IPINV (DES-IP x)) . 64 = (DES-IP x) . 25 ) by Def16;
for i being object st i in Seg 64 holds
(DES-IPINV (DES-IP x)) . i = x . i

proof

let i be object ; :: thesis: ( i in Seg 64 implies (DES-IPINV (DES-IP x)) . i = x . i )
assume i in Seg 64 ; :: thesis: (DES-IPINV (DES-IP x)) . i = x . i
then not not i = 1 & ... & not i = 64 by FINSEQ_1:91;
hence (DES-IPINV (DES-IP x)) . i = x . i by A2, Def14; :: thesis: verum

end;

hence DES-IPINV (DES-IP x) = x by A1; :: thesis: verum