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 A8: 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
A9: ( q = s & len s = 16 ) ;
A10: dom q = Seg 16 by A9, FINSEQ_1:def 3;
given C1, D1 being sequence of (28 -tuples_on BOOLEAN) such that A11: ( 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 A12: ( 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₁[ 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) ) );
A13: S₁[ 0 ]

proof

A14: C1 . (0 + 1) = Op-Shift ((C2 . 0),(bitshift_DES . 0)) by A11, A12
.= C2 . (0 + 1) by A12 ;
A15: D1 . (0 + 1) = Op-Shift ((D2 . 0),(bitshift_DES . 0)) by A11, A12
.= D2 . (0 + 1) by A12 ;
p . (0 + 1) = DES-PC2 ((C2 . (0 + 1)) ^ (D2 . (0 + 1))) by A14, A15, A11
.= q . (0 + 1) by A12 ;
hence S₁[ 0 ] by A14, A15; :: thesis: verum

end;

A16: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A17: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[i + 1] :: thesis: verum

proof

assume A18: ( 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) )
A19: i <= i + 1 by NAT_1:12;
A20: C1 . ((i + 1) + 1) = Op-Shift ((C2 . (i + 1)),(bitshift_DES . (i + 1))) by A19, A17, A18, A11, XXREAL_0:2
.= C2 . ((i + 1) + 1) by A12, A18 ;
A21: D1 . ((i + 1) + 1) = Op-Shift ((D2 . (i + 1)),(bitshift_DES . (i + 1))) by A19, A17, A18, A11, XXREAL_0:2
.= D2 . ((i + 1) + 1) by A12, A18 ;
p . ((i + 1) + 1) = DES-PC2 ((C2 . ((i + 1) + 1)) ^ (D2 . ((i + 1) + 1))) by A20, A21, A11, A18
.= q . ((i + 1) + 1) by A12, A18 ;
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 A20, A21; :: thesis: verum

end;

end;

A22: for i being Nat holds S₁[i] from NAT_1:sch 2(A13, A16);
for i being object st i in dom p holds
p . i = q . i

proof

let i be object ; :: thesis: ( i in dom p implies p . i = q . i )
assume A23: i in dom p ; :: thesis: p . i = q . i
reconsider i = i as Element of NAT by A23;
A24: ( 1 <= i & i <= 16 ) by A23, A8, 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 A24, XREAL_1:9;
then p . (y + 1) = q . (y + 1) by A22;
hence p . i = q . i ; :: thesis: verum

end;

hence p = q by A8, A10; :: thesis: verum