environ
vocabularies HIDDEN, NUMBERS, QUATERNI, ORDINAL1, SUBSET_1, RELAT_1, ARYTM_1, ARYTM_3, ARYTM_0, REAL_1, CARD_1, XCMPLX_0, COMPLEX1, SQUARE_1, XXREAL_0, POLYEQ_3, FUNCT_7;
notations HIDDEN, SUBSET_1, ORDINAL1, FUNCT_7, NUMBERS, XXREAL_0, XCMPLX_0, COMPLEX1, XREAL_0, ARYTM_0, QUATERNI, REAL_1, SQUARE_1, QUATERN2;
definitions ;
theorems ARYTM_0, SQUARE_1, XREAL_1, QUATERNI, QUATERN2, XCMPLX_1, XREAL_0;
schemes ;
registrations MEMBERED, QUATERNI, XREAL_0, SQUARE_1;
constructors HIDDEN, FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, COMPLEX1, RFUNCT_1, QUATERN2, FUNCT_7, NUMBERS;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities SQUARE_1, XCMPLX_0, QUATERNI;
expansions ;
Lm1:
for z being quaternion number st z is Real holds
( z = Rea z & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 )
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm2:
<i> = [*(In (0,REAL)),jj*]
by ARYTM_0:def 5;