let H1, H2 be Function of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))); :: thesis: ( ( for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (H1 . input) . i = Op-Shift (xi,(5 - i)) ) ) & ( for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (H2 . input) . i = Op-Shift (xi,(5 - i)) ) ) implies H1 = H2 )
assume A1: for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (H1 . input) . i = Op-Shift (xi,(5 - i)) ) ; :: thesis: ( ex input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex i being Nat st
( i in Seg 4 & ( for xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) holds
( not xi = input . i or not (H2 . input) . i = Op-Shift (xi,(5 - i)) ) ) ) or H1 = H2 )
assume A2: for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i being Nat st i in Seg 4 holds
ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (H2 . input) . i = Op-Shift (xi,(5 - i)) ) ; :: thesis: H1 = H2
now :: thesis: for input being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds H1 . input = H2 . input
let input be Element of 4 -tuples_on (4 -tuples_on (8 -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 XX2: i in Seg 4 by P3;
then XX3: ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (H1 . input) . i = Op-Shift (xi,(5 - i)) ) by A1;
XX4: ex xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( xi = input . i & (H2 . input) . i = Op-Shift (xi,(5 - i)) ) by A2, XX2;
thus (H1 . input) . i = (H2 . input) . i by XX3, XX4; :: thesis: verum
end;
hence H1 . input = H2 . input by P3, P4, FINSEQ_1:14; :: thesis: verum
end;
hence H1 = H2 by FUNCT_2:63; :: thesis: verum