let H1, H2 be Function of (128 -tuples_on BOOLEAN),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))); :: thesis: ( ( for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((H1 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ) & ( for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((H2 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ) implies H1 = H2 )
assume A1: for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((H1 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ; :: thesis: ( ex input being Element of 128 -tuples_on BOOLEAN ex i, j being Nat st
( i in Seg 4 & j in Seg 4 & not ((H2 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ) or H1 = H2 )
assume A2: for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((H2 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) ; :: thesis: H1 = H2
now :: thesis: for input being Element of 128 -tuples_on BOOLEAN holds H1 . input = H2 . input
let input be Element of 128 -tuples_on BOOLEAN; :: thesis: H1 . input = H2 . input
H1 . input in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then P3: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( H1 . input = s & len s = 4 ) ;
H2 . input in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then P4: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( H2 . input = s & len s = 4 ) ;
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 ( 1 <= i & i <= len (H1 . input) ) ; :: thesis: (H1 . input) . i = (H2 . input) . i
then P6: i in Seg 4 by P3;
then i in dom (H1 . input) by FINSEQ_1:def 3, P3;
then (H1 . input) . i in rng (H1 . input) by FUNCT_1:3;
then (H1 . input) . i in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then P8: ex s being Element of (8 -tuples_on BOOLEAN) * st
( (H1 . input) . i = s & len s = 4 ) ;
reconsider H1i = (H1 . input) . i as Element of (8 -tuples_on BOOLEAN) * by P8;
i in dom (H2 . input) by FINSEQ_1:def 3, P4, P6;
then (H2 . input) . i in rng (H2 . input) by FUNCT_1:3;
then (H2 . input) . i in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then P11: ex s being Element of (8 -tuples_on BOOLEAN) * st
( (H2 . input) . i = s & len s = 4 ) ;
reconsider H2i = (H2 . input) . i as Element of (8 -tuples_on BOOLEAN) * by P11;
now :: thesis: for j being Nat st 1 <= j & j <= len H1i holds
H1i . j = H2i . j
let j be Nat; :: thesis: ( 1 <= j & j <= len H1i implies H1i . j = H2i . j )
assume ( 1 <= j & j <= len H1i ) ; :: thesis: H1i . j = H2i . j
then P14: j in Seg 4 by P8;
then ((H1 . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) by A1, P6;
hence H1i . j = H2i . j by A2, P6, P14; :: thesis: verum
end;
hence (H1 . input) . i = (H2 . input) . i by P8, P11, FINSEQ_1:def 17; :: thesis: verum
end;
hence H1 . input = H2 . input by P3, P4, FINSEQ_1:def 17; :: thesis: verum
end;
hence H1 = H2 by FUNCT_2:63; :: thesis: verum