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 ASP: ( 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 ASQ: ( 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
CT: ( 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
CS: ( q = s & len s = 8 ) ;
L1: ( dom p = Seg 8 & dom q = Seg 8 ) by CT, CS, 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 L1, ENUMSET1:def 6, FINSEQ_3:6;
hence p . i = q . i by ASP, ASQ; :: thesis: verum

end;

hence p = q by L1, FINSEQ_1:13; :: thesis: verum