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