let H1, H2 be Element of 4 -tuples_on (8 -tuples_on BOOLEAN); :: thesis: ( ( for i being Element of Seg 4 holds H1 . i = SBT . (x . i) ) & ( for i being Element of Seg 4 holds H2 . i = SBT . (x . i) ) implies H1 = H2 )
assume A1: for i being Element of Seg 4 holds H1 . i = SBT . (x . i) ; :: thesis: ( ex i being Element of Seg 4 st not H2 . i = SBT . (x . i) or H1 = H2 )
assume A2: for i being Element of Seg 4 holds H2 . i = SBT . (x . i) ; :: thesis: H1 = H2
H1 in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then P1: ex s being Element of (8 -tuples_on BOOLEAN) * st
( H1 = s & len s = 4 ) ;
H2 in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then P2: ex s being Element of (8 -tuples_on BOOLEAN) * st
( H2 = s & len s = 4 ) ;
now :: thesis: for i being Nat st 1 <= i & i <= len H1 holds
H1 . i = H2 . i
let i be Nat; :: thesis: ( 1 <= i & i <= len H1 implies H1 . i = H2 . i )
assume ( 1 <= i & i <= len H1 ) ; :: thesis: H1 . i = H2 . i
then i in Seg 4 by P1;
then reconsider j = i as Element of Seg 4 ;
thus H1 . i = SBT . (x . j) by A1
.= H2 . i by A2 ; :: thesis: verum
end;
hence H1 = H2 by P1, P2, FINSEQ_1:14; :: thesis: verum