let H1, H2 be Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))); ( ( for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(H1 . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) ) ) & ( for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(H2 . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) ) ) implies H1 = H2 )
assume A1:
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(H1 . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) )
; ( ex Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
for w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( not w = (KeyExpansionX (SBT,m)) . Key or ex i being Nat st
( i < 7 + m & not (H2 . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) ) or H1 = H2 )
assume A2:
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(H2 . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) )
; H1 = H2
now for input being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds H1 . input = H2 . inputlet input be
Element of
m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN));
H1 . input = H2 . inputconsider w1 being
Element of
(4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that P1:
(
w1 = (KeyExpansionX (SBT,m)) . input & ( for
i being
Nat st
i < 7
+ m holds
(H1 . input) . (i + 1) = <*(w1 . ((4 * i) + 1)),(w1 . ((4 * i) + 2)),(w1 . ((4 * i) + 3)),(w1 . ((4 * i) + 4))*> ) )
by A1;
consider w2 being
Element of
(4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that P2:
(
w2 = (KeyExpansionX (SBT,m)) . input & ( for
i being
Nat st
i < 7
+ m holds
(H2 . input) . (i + 1) = <*(w2 . ((4 * i) + 1)),(w2 . ((4 * i) + 2)),(w2 . ((4 * i) + 3)),(w2 . ((4 * i) + 4))*> ) )
by A2;
H1 . input in (7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
;
then P3:
ex
s being
Element of
(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) * st
(
H1 . input = s &
len s = 7
+ m )
;
H2 . input in (7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
;
then P4:
ex
s being
Element of
(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) * st
(
H2 . input = s &
len s = 7
+ m )
;
now for i being Nat st 1 <= i & i <= len (H1 . input) holds
(H1 . input) . i = (H2 . input) . iend; hence
H1 . input = H2 . input
by P3, P4, FINSEQ_1:def 17;
verum end;
hence
H1 = H2
by FUNCT_2:63; verum