let p, q be Element of 8 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); ( p . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & p . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & p . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & p . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & p . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & p . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> & p . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & p . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> & q . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & q . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & q . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & q . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & q . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & q . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> & q . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & q . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> implies p = q )
assume A6:
( p . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & p . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & p . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & p . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & p . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & p . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> & p . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & p . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> )
; ( not q . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> or not q . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> or not q . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> or not q . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> or not q . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> or not q . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> or not q . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> or not q . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> or p = q )
assume A7:
( q . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & q . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & q . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & q . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & q . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & q . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Left ((Op-Right (r,184)),8))*> & q . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & q . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> )
; p = q
p in 8 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
;
then A8:
ex v being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( p = v & len v = 8 )
;
q in 8 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
;
then A9:
ex v being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( q = v & len v = 8 )
;
for i being Nat st 1 <= i & i <= len p holds
p . i = q . i
proof
let i be
Nat;
( 1 <= i & i <= len p implies p . i = q . i )
assume
( 1
<= i &
i <= len p )
;
p . i = q . i
then
not not
i = 1 & ... & not
i = 8
by A8;
hence
p . i = q . i
by A6, A7;
verum
end;
hence
p = q
by A8, A9, FINSEQ_1:14; verum