( H is being_equality or H is being_membership ) by A1;
then consider k being Element of NAT , x, y being Variable such that
A2: H = (<*k*> ^ <*x*>) ^ <*y*> ;
H = <*k,x,y*> by A2, FINSEQ_1:def 10;
hence H . 2 is Variable by FINSEQ_1:45; :: thesis: verum