let p, q be Element of 8 -tuples_on (6 -tuples_on BOOLEAN); :: thesis: ( p . 1 = Op-Left (r,6) & p . 2 = Op-Left ((Op-Right (r,6)),6) & p . 3 = Op-Left ((Op-Right (r,12)),6) & p . 4 = Op-Left ((Op-Right (r,18)),6) & p . 5 = Op-Left ((Op-Right (r,24)),6) & p . 6 = Op-Left ((Op-Right (r,30)),6) & p . 7 = Op-Left ((Op-Right (r,36)),6) & p . 8 = Op-Right (r,42) & q . 1 = Op-Left (r,6) & q . 2 = Op-Left ((Op-Right (r,6)),6) & q . 3 = Op-Left ((Op-Right (r,12)),6) & q . 4 = Op-Left ((Op-Right (r,18)),6) & q . 5 = Op-Left ((Op-Right (r,24)),6) & q . 6 = Op-Left ((Op-Right (r,30)),6) & q . 7 = Op-Left ((Op-Right (r,36)),6) & q . 8 = Op-Right (r,42) implies p = q )
assume A6: ( p . 1 = Op-Left (r,6) & p . 2 = Op-Left ((Op-Right (r,6)),6) & p . 3 = Op-Left ((Op-Right (r,12)),6) & p . 4 = Op-Left ((Op-Right (r,18)),6) & p . 5 = Op-Left ((Op-Right (r,24)),6) & p . 6 = Op-Left ((Op-Right (r,30)),6) & p . 7 = Op-Left ((Op-Right (r,36)),6) & p . 8 = Op-Right (r,42) ) ; :: thesis: ( not q . 1 = Op-Left (r,6) or not q . 2 = Op-Left ((Op-Right (r,6)),6) or not q . 3 = Op-Left ((Op-Right (r,12)),6) or not q . 4 = Op-Left ((Op-Right (r,18)),6) or not q . 5 = Op-Left ((Op-Right (r,24)),6) or not q . 6 = Op-Left ((Op-Right (r,30)),6) or not q . 7 = Op-Left ((Op-Right (r,36)),6) or not q . 8 = Op-Right (r,42) or p = q )
assume A7: ( q . 1 = Op-Left (r,6) & q . 2 = Op-Left ((Op-Right (r,6)),6) & q . 3 = Op-Left ((Op-Right (r,12)),6) & q . 4 = Op-Left ((Op-Right (r,18)),6) & q . 5 = Op-Left ((Op-Right (r,24)),6) & q . 6 = Op-Left ((Op-Right (r,30)),6) & q . 7 = Op-Left ((Op-Right (r,36)),6) & q . 8 = Op-Right (r,42) ) ; :: thesis: p = q
p in { s where s is Element of (6 -tuples_on BOOLEAN) * : len s = 8 } ;
then consider t being Element of (6 -tuples_on BOOLEAN) * such that
A8: ( p = t & len t = 8 ) ;
q in { s where s is Element of (6 -tuples_on BOOLEAN) * : len s = 8 } ;
then consider s being Element of (6 -tuples_on BOOLEAN) * such that
A9: ( q = s & len s = 8 ) ;
A10: ( dom p = Seg 8 & dom q = Seg 8 ) by A8, A9, FINSEQ_1:def 3;
for i being Nat st i in dom p holds
p . i = q . i

proof

let i be Nat; :: thesis: ( i in dom p implies p . i = q . i )
assume i in dom p ; :: thesis: p . i = q . i
then ( i = 1 or i = 2 or i = 3 or i = 4 or i = 5 or i = 6 or i = 7 or i = 8 ) by A10, ENUMSET1:def 6, FINSEQ_3:6;
hence p . i = q . i by A6, A7; :: thesis: verum

end;

hence p = q by A10; :: thesis: verum