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

(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