set X = { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ;

A1: now :: thesis: not <j> in { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) }

assume <j> in { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } ; :: thesis: contradiction
then ex x being Element of Funcs (4,REAL) st
( <j> = x & x . 2 = 0 & x . 3 = 0 ) ;
hence contradiction by FUNCT_4:140; :: thesis: verum

end;

reconsider z = 0 , j = 0 , w = 1, m = 0 as Element of REAL by XREAL_0:def 1;
<j> = (0,1,2,3) --> (z,j,w,m) ;
then <j> in Funcs (4,REAL) by CARD_1:52, FUNCT_2:8;
then <j> in (Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } by A1, XBOOLE_0:def 5;
hence <j> in QUATERNION by XBOOLE_0:def 3; :: according to QUATERNI:def 2 :: thesis: verum