A5: ( H is being_equality or H is being_membership ) by A1, Def15;
A6: ( ex x, y being Variable st H = x '=' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ;
( ex x, y being Variable st H = x 'in' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ;
then consider k being Element of NAT , x, y being Variable such that
A7: H = (<*k*> ^ <*x*>) ^ <*y*> by A5, A6, Def10, Def11;
H = <*k,x,y*> by A7, FINSEQ_1:def 10;
hence H . 3 is Variable by FINSEQ_1:62; :: thesis: verum