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

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

assume <k> 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
( <k> = x & x . 2 = 0 & x . 3 = 0 ) ;
hence contradiction by FUNCT_4:139; :: thesis: verum

end;

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