let R1, R2 be Element of 10 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); ( R1 . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> implies R1 = R2 )
assume A1:
( R1 . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R1 . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> )
; ( not R2 . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> or not R2 . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> or not R2 . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> or not R2 . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> or not R2 . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> or not R2 . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> or not R2 . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> or not R2 . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> or not R2 . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> or not R2 . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> or R1 = R2 )
assume A2:
( R2 . 1 = <*(<*0,0,0,0*> ^ <*0,0,0,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 2 = <*(<*0,0,0,0*> ^ <*0,0,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 3 = <*(<*0,0,0,0*> ^ <*0,1,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 4 = <*(<*0,0,0,0*> ^ <*1,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 5 = <*(<*0,0,0,1*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 6 = <*(<*0,0,1,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 7 = <*(<*0,1,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 8 = <*(<*1,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 9 = <*(<*0,0,0,1*> ^ <*1,0,1,1*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> & R2 . 10 = <*(<*0,0,1,1*> ^ <*0,1,1,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>),(<*0,0,0,0*> ^ <*0,0,0,0*>)*> )
; R1 = R2
R1 in 10 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
;
then XP1:
ex v being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( R1 = v & len v = 10 )
;
R2 in 10 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
;
then XP2:
ex v being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( R2 = v & len v = 10 )
;
for i being Nat st 1 <= i & i <= len R1 holds
R1 . i = R2 . i
proof
let i be
Nat;
( 1 <= i & i <= len R1 implies R1 . i = R2 . i )
assume
( 1
<= i &
i <= len R1 )
;
R1 . i = R2 . i
then
not not
i = 1 & ... & not
i = 10
by XP1;
hence
R1 . i = R2 . i
by A1, A2;
verum
end;
hence
R1 = R2
by XP1, XP2, FINSEQ_1:14; verum