let L be non empty ZeroStr ; 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; ( <%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
; ( <%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
; ( <%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; for n being Nat st n >= 3 holds
<%c,b,a%> . n = 0. L
let n be Nat; ( n >= 3 implies <%c,b,a%> . n = 0. L )
assume A3:
n >= 3
; <%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
; verum