let p, q be Element of 16 -tuples_on (48 -tuples_on BOOLEAN); :: thesis: ( ex C, D being sequence of (28 -tuples_on BOOLEAN) st
( C . 0 = Op-Left ((DES-PC1 Key),28) & D . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( p . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) ) ) & ex C, D being sequence of (28 -tuples_on BOOLEAN) st
( C . 0 = Op-Left ((DES-PC1 Key),28) & D . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( q . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) ) ) implies p = q )
len p = 16 by CARD_1:def 7;
then LDOMP: dom p = Seg 16 by FINSEQ_1:def 3;
q in { s where s is Element of (48 -tuples_on BOOLEAN) * : len s = 16 } ;
then consider s being Element of (48 -tuples_on BOOLEAN) * such that
CS: ( q = s & len s = 16 ) ;
LDOMQ: dom q = Seg 16 by CS, FINSEQ_1:def 3;
given C1, D1 being sequence of (28 -tuples_on BOOLEAN) such that A3: ( C1 . 0 = Op-Left ((DES-PC1 Key),28) & D1 . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( p . (i + 1) = DES-PC2 ((C1 . (i + 1)) ^ (D1 . (i + 1))) & C1 . (i + 1) = Op-Shift ((C1 . i),(bitshift_DES . i)) & D1 . (i + 1) = Op-Shift ((D1 . i),(bitshift_DES . i)) ) ) ) ; :: thesis: ( for C, D being sequence of (28 -tuples_on BOOLEAN) holds
( not C . 0 = Op-Left ((DES-PC1 Key),28) or not D . 0 = Op-Right ((DES-PC1 Key),28) or ex i being Element of NAT st
( 0 <= i & i <= 15 & not ( q . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) ) ) or p = q )
given C2, D2 being sequence of (28 -tuples_on BOOLEAN) such that A4: ( C2 . 0 = Op-Left ((DES-PC1 Key),28) & D2 . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( q . (i + 1) = DES-PC2 ((C2 . (i + 1)) ^ (D2 . (i + 1))) & C2 . (i + 1) = Op-Shift ((C2 . i),(bitshift_DES . i)) & D2 . (i + 1) = Op-Shift ((D2 . i),(bitshift_DES . i)) ) ) ) ; :: thesis: p = q
defpred S₁[ Element of NAT ] means ( 0 <= $1 & $1 <= 15 implies ( p . ($1 + 1) = q . ($1 + 1) & C1 . ($1 + 1) = C2 . ($1 + 1) & D1 . ($1 + 1) = D2 . ($1 + 1) ) );
P0: S₁[ 0 ]

proof

Q2: C1 . (0 + 1) = Op-Shift ((C2 . 0),(bitshift_DES . 0)) by A3, A4
.= C2 . (0 + 1) by A4 ;
Q3: D1 . (0 + 1) = Op-Shift ((D2 . 0),(bitshift_DES . 0)) by A3, A4
.= D2 . (0 + 1) by A4 ;
p . (0 + 1) = DES-PC2 ((C2 . (0 + 1)) ^ (D2 . (0 + 1))) by Q2, Q3, A3
.= q . (0 + 1) by A4 ;
hence S₁[ 0 ] by Q2, Q3; :: thesis: verum

end;

P1: now :: thesis: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume P11: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[i + 1] :: thesis: verum

proof

assume P12: ( 0 <= i + 1 & i + 1 <= 15 ) ; :: thesis: ( p . ((i + 1) + 1) = q . ((i + 1) + 1) & C1 . ((i + 1) + 1) = C2 . ((i + 1) + 1) & D1 . ((i + 1) + 1) = D2 . ((i + 1) + 1) )
P14P: i <= i + 1 by NAT_1:12;
Q2: C1 . ((i + 1) + 1) = Op-Shift ((C2 . (i + 1)),(bitshift_DES . (i + 1))) by P14P, P11, P12, A3, XXREAL_0:2
.= C2 . ((i + 1) + 1) by A4, P12 ;
Q3: D1 . ((i + 1) + 1) = Op-Shift ((D2 . (i + 1)),(bitshift_DES . (i + 1))) by P14P, P11, P12, A3, XXREAL_0:2
.= D2 . ((i + 1) + 1) by A4, P12 ;
p . ((i + 1) + 1) = DES-PC2 ((C2 . ((i + 1) + 1)) ^ (D2 . ((i + 1) + 1))) by Q2, Q3, A3, P12
.= q . ((i + 1) + 1) by A4, P12 ;
hence ( p . ((i + 1) + 1) = q . ((i + 1) + 1) & C1 . ((i + 1) + 1) = C2 . ((i + 1) + 1) & D1 . ((i + 1) + 1) = D2 . ((i + 1) + 1) ) by Q2, Q3; :: thesis: verum

end;

end;

LP1P: for i being Element of NAT holds S₁[i] from NAT_1:sch 1(P0, P1);
for i being set st i in dom p holds
p . i = q . i

proof

let i be set ; :: thesis: ( i in dom p implies p . i = q . i )
assume LL1P: i in dom p ; :: thesis: p . i = q . i
reconsider i = i as Element of NAT by LL1P;
LL2: ( 1 <= i & i <= 16 ) by LL1P, LDOMP, FINSEQ_1:1;
then reconsider y = i - 1 as Element of NAT by NAT_1:21;
( 1 - 1 <= i - 1 & i - 1 <= 16 - 1 ) by LL2, XREAL_1:9;
then p . (y + 1) = q . (y + 1) by LP1P;
hence p . i = q . i ; :: thesis: verum

end;

hence p = q by LDOMP, LDOMQ, FUNCT_1:2; :: thesis: verum