let L be non empty multLoopStr_0 ; :: thesis: ( (1_. L) . 0 = 1. L & ( for n being Nat st n <> 0 holds
(1_. L) . n = 0. L ) )
0 in NAT ;
then 0 in dom (0_. L) by FUNCT_2:def 1;
hence (1_. L) . 0 = 1. L by FUNCT_7:31; :: thesis: for n being Nat st n <> 0 holds
(1_. L) . n = 0. L
let n be Nat; :: thesis: ( n <> 0 implies (1_. L) . n = 0. L )
A1: n in NAT by ORDINAL1:def 12;
assume n <> 0 ; :: thesis: (1_. L) . n = 0. L
hence (1_. L) . n = (0_. L) . n by FUNCT_7:32
.= 0. L by A1, FUNCOP_1:7 ;
:: thesis: verum