let R1, R2 be Element of 10 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ( 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*>)*> ) ; :: thesis: ( 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*>)*> ) ; :: thesis: 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; :: thesis: ( 1 <= i & i <= len R1 implies R1 . i = R2 . i )
assume ( 1 <= i & i <= len R1 ) ; :: thesis: R1 . i = R2 . i
then not not i = 1 & ... & not i = 10 by XP1;
hence R1 . i = R2 . i by A1, A2; :: thesis: verum

end;

hence R1 = R2 by XP1, XP2, FINSEQ_1:14; :: thesis: verum