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

A2: now

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

end;

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