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 L1: ( dom x = Seg 64 & dom (DES-IPINV (DES-IP x)) = Seg 64 ) by FINSEQ_1:def 3;
LI1: ( (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 defIPINV;
for i being set st i in Seg 64 holds
(DES-IPINV (DES-IP x)) . i = x . i

proof

let i be set ; :: 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 ( i = 1 or i = 2 or i = 3 or i = 4 or i = 5 or i = 6 or i = 7 or i = 8 or i = 9 or i = 10 or i = 11 or i = 12 or i = 13 or i = 14 or i = 15 or i = 16 or i = 17 or i = 18 or i = 19 or i = 20 or i = 21 or i = 22 or i = 23 or i = 24 or i = 25 or i = 26 or i = 27 or i = 28 or i = 29 or i = 30 or i = 31 or i = 32 or i = 33 or i = 34 or i = 35 or i = 36 or i = 37 or i = 38 or i = 39 or i = 40 or i = 41 or i = 42 or i = 43 or i = 44 or i = 45 or i = 46 or i = 47 or i = 48 or i = 49 or i = 50 or i = 51 or i = 52 or i = 53 or i = 54 or i = 55 or i = 56 or i = 57 or i = 58 or i = 59 or i = 60 or i = 61 or i = 62 or i = 63 or i = 64 ) by Lmseg64a;
hence (DES-IPINV (DES-IP x)) . i = x . i by LI1, defIP; :: thesis: verum

end;

hence DES-IPINV (DES-IP x) = x by L1, FUNCT_1:2; :: thesis: verum