let L be non empty ZeroStr ; :: thesis: for a, b, c being Element of L holds
( <%c,b,a%> . 0 = c & <%c,b,a%> . 1 = b & <%c,b,a%> . 2 = a & ( for n being Nat st n >= 3 holds
<%c,b,a%> . n = 0. L ) )
let a, b, c be Element of L; :: thesis: ( <%c,b,a%> . 0 = c & <%c,b,a%> . 1 = b & <%c,b,a%> . 2 = a & ( for n being Nat st n >= 3 holds
<%c,b,a%> . n = 0. L ) )
A1: 0 in dom (0_. L) ;
thus <%c,b,a%> . 0 = (((0_. L) +* (0,c)) +* (1,b)) . 0 by FUNCT_7:32
.= ((0_. L) +* (0,c)) . 0 by FUNCT_7:32
.= c by A1, FUNCT_7:31 ; :: thesis: ( <%c,b,a%> . 1 = b & <%c,b,a%> . 2 = a & ( for n being Nat st n >= 3 holds
<%c,b,a%> . n = 0. L ) )
1 in NAT ;
then H: 1 in dom ((0_. L) +* (0,c)) by FUNCT_2:def 1;
thus <%c,b,a%> . 1 = (((0_. L) +* (0,c)) +* (1,b)) . 1 by FUNCT_7:32
.= b by H, FUNCT_7:31 ; :: thesis: ( <%c,b,a%> . 2 = a & ( for n being Nat st n >= 3 holds
<%c,b,a%> . n = 0. L ) )
A2: 2 in NAT ;
2 in dom (((0_. L) +* (0,c)) +* (1,b)) by A2, FUNCT_2:def 1;
hence <%c,b,a%> . 2 = a by FUNCT_7:31; :: thesis: for n being Nat st n >= 3 holds
<%c,b,a%> . n = 0. L
let n be Nat; :: thesis: ( n >= 3 implies <%c,b,a%> . n = 0. L )
assume A3: n >= 3 ; :: thesis: <%c,b,a%> . n = 0. L
then n >= (1 + 1) + 1 ;
then H1: n > (0 + 1) + 1 by NAT_1:13;
then H2: n > 0 + 1 by NAT_1:13;
thus <%c,b,a%> . n = (((0_. L) +* (0,c)) +* (1,b)) . n by H1, FUNCT_7:32
.= ((0_. L) +* (0,c)) . n by H2, FUNCT_7:32
.= (0_. L) . n by A3, FUNCT_7:32
.= 0. L by ORDINAL1:def 12, FUNCOP_1:7 ; :: thesis: verum