set z1 = 0 ;
set z2 = <i> ;
consider y1, y2, y3, y4 being Real such that
A1: ( <i> = [*y1,y2,y3,y4*] & 0 * <i> = [*(0 * y1),(0 * y2),(0 * y3),(0 * y4)*] ) by Def20;
A2: 0 * <i> = [*(In (0,REAL)),(In (0,REAL))*] by A1, Lm3
.= 0 by ARYTM_0:def 5 ;
consider y1, y2, y3, y4 being Real such that
A3: ( <j> = [*y1,y2,y3,y4*] & 0 * <j> = [*(0 * y1),(0 * y2),(0 * y3),(0 * y4)*] ) by Def20;
A4: 0 * <j> = [*(In (0,REAL)),(In (0,REAL))*] by A3, Lm3
.= 0 by ARYTM_0:def 5 ;
consider y1, y2, y3, y4 being Real such that
A5: ( <k> = [*y1,y2,y3,y4*] & 0 * <k> = [*(0 * y1),(0 * y2),(0 * y3),(0 * y4)*] ) by Def20;
0 * <k> = [*(In (0,REAL)),(In (0,REAL))*] by A5, Lm3
.= 0 by ARYTM_0:def 5 ;
hence ( 0 * <i> = 0 & 0 * <j> = 0 & 0 * <k> = 0 ) by A2, A4; :: thesis: verum