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

A1: now

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 Lm1, Th3; :: thesis: verum

end;

reconsider z = 0 , j = 0 , w = 1, m = 0 as Element of REAL ;
<j> = 0 ,1,2,3 --> z,j,w,m ;
then <j> in Funcs 4,REAL by CARD_1:90, FUNCT_2:11;
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