set z1 = 0 ;
set z2 = <i> ;
consider y1, y2, y3, y4 being Element of REAL such that
A1: ( <i> = [*y1,y2,y3,y4*] & 0 * <i> = [*(0 * y1),(0 * y2),(0 * y3),(0 * y4)*] ) by Def21;
A2: 0 * <i> = [*0,0*] by A1, Lm4
.= 0 by ARYTM_0:def 7 ;
consider y1, y2, y3, y4 being Element of REAL such that
A1: ( <j> = [*y1,y2,y3,y4*] & 0 * <j> = [*(0 * y1),(0 * y2),(0 * y3),(0 * y4)*] ) by Def21;
A3: 0 * <j> = [*0,0*] by A1, Lm4
.= 0 by ARYTM_0:def 7 ;
consider y1, y2, y3, y4 being Element of REAL such that
A1: ( <k> = [*y1,y2,y3,y4*] & 0 * <k> = [*(0 * y1),(0 * y2),(0 * y3),(0 * y4)*] ) by Def21;
0 * <k> = [*0,0*] by A1, Lm4
.= 0 by ARYTM_0:def 7 ;
hence ( 0 * <i> = 0 & 0 * <j> = 0 & 0 * <k> = 0 ) by A2, A3; :: thesis: verum