let H1, H2 be Element of m -tuples_on (n -tuples_on BOOLEAN); :: thesis: ( ( for i being Element of Seg m holds H1 . i = Op-XOR ((s . i),(t . i)) ) & ( for i being Element of Seg m holds H2 . i = Op-XOR ((s . i),(t . i)) ) implies H1 = H2 )
assume A1: for i being Element of Seg m holds H1 . i = Op-XOR ((s . i),(t . i)) ; :: thesis: ( ex i being Element of Seg m st not H2 . i = Op-XOR ((s . i),(t . i)) or H1 = H2 )
assume A2: for i being Element of Seg m holds H2 . i = Op-XOR ((s . i),(t . i)) ; :: thesis: H1 = H2
H1 in m -tuples_on (n -tuples_on BOOLEAN) ;
then P1: ex v being Element of (n -tuples_on BOOLEAN) * st
( H1 = v & len v = m ) ;
H2 in m -tuples_on (n -tuples_on BOOLEAN) ;
then P2: ex v being Element of (n -tuples_on BOOLEAN) * st
( H2 = v & len v = m ) ;

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 m by P1;
then reconsider j = i as Element of Seg m ;
thus H1 . i = Op-XOR ((s . j),(t . j)) by A1
.= H2 . i by A2 ; :: thesis: verum

end;

hence H1 = H2 by P1, P2, FINSEQ_1:14; :: thesis: verum