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)))); :: thesis: ( ( 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))*> ) ) ; :: thesis: ( 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))*> ) ) ; :: thesis: H1 = H2

now :: thesis: for input being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds H1 . input = H2 . input

let input be Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: H1 . input = H2 . input
consider 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 :: thesis: for i being Nat st 1 <= i & i <= len (H1 . input) holds
(H1 . input) . i = (H2 . input) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (H1 . input) implies (H1 . input) . i = (H2 . input) . i )
assume P5: ( 1 <= i & i <= len (H1 . input) ) ; :: thesis: (H1 . input) . i = (H2 . input) . i
then i - 1 in NAT by XREAL_1:48, INT_1:3;
then reconsider i0 = i - 1 as Nat ;
i < (7 + m) + 1 by P3, P5, NAT_1:13;
then P6: i - 1 < ((7 + m) + 1) - 1 by XREAL_1:14;
thus (H1 . input) . i = (H1 . input) . (i0 + 1)
.= <*(w2 . ((4 * i0) + 1)),(w2 . ((4 * i0) + 2)),(w2 . ((4 * i0) + 3)),(w2 . ((4 * i0) + 4))*> by P6, P1, P2
.= (H2 . input) . (i0 + 1) by P6, P2
.= (H2 . input) . i ; :: thesis: verum

end;

hence H1 . input = H2 . input by P3, P4, FINSEQ_1:def 18; :: thesis: verum

end;

hence H1 = H2 by FUNCT_2:63; :: thesis: verum