A2: ( 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*> ) ;
A3: ( 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*> ) ;
( H is being_equality or H is being_membership ) by A1, Def15;
then consider k being Element of NAT , x, y being Variable such that
A4: H = (<*k*> ^ <*x*>) ^ <*y*> by A3, A2, Def10, Def11;
H = <*k,x,y*> by A4, FINSEQ_1:def 10;
hence H . 2 is Variable by FINSEQ_1:62; :: thesis: verum