thus ( z in COMPLEX implies ex IT being Number st IT = 0 ) ; :: thesis: ( not z in COMPLEX implies ex b₁ being Number ex f being Function of 4,REAL st
( z = f & b₁ = f . 2 ) )
assume A5: not z in COMPLEX ; :: thesis: ex b₁ being Number ex f being Function of 4,REAL st
( z = f & b₁ = f . 2 )
z in QUATERNION by Def2;
then z in (Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } by A5, XBOOLE_0:def 3;
then reconsider f = z as Function of 4,REAL by FUNCT_2:66;
take f . 2 ; :: thesis: ex f being Function of 4,REAL st
( z = f & f . 2 = f . 2 )
take f ; :: thesis: ( z = f & f . 2 = f . 2 )
thus ( z = f & f . 2 = f . 2 ) ; :: thesis: verum