let L be non empty right_complementable add-associative right_zeroed addLoopStr ; for F being FinSequence of L
for G being FinSequence
for k being Nat st G = F | (Seg k) & len F = k + 1 holds
( G is FinSequence of L & dom G c= dom F & len G = k & F = G ^ <*(F /. (k + 1))*> )
let F be FinSequence of L; for G being FinSequence
for k being Nat st G = F | (Seg k) & len F = k + 1 holds
( G is FinSequence of L & dom G c= dom F & len G = k & F = G ^ <*(F /. (k + 1))*> )
let G1 be FinSequence; for k being Nat st G1 = F | (Seg k) & len F = k + 1 holds
( G1 is FinSequence of L & dom G1 c= dom F & len G1 = k & F = G1 ^ <*(F /. (k + 1))*> )
let k be Nat; ( G1 = F | (Seg k) & len F = k + 1 implies ( G1 is FinSequence of L & dom G1 c= dom F & len G1 = k & F = G1 ^ <*(F /. (k + 1))*> ) )
assume that
A1:
G1 = F | (Seg k)
and
A2:
len F = k + 1
; ( G1 is FinSequence of L & dom G1 c= dom F & len G1 = k & F = G1 ^ <*(F /. (k + 1))*> )
reconsider G = G1 as FinSequence ;
A3:
k <= len F
by A2, NAT_1:13;
then A4:
len G = k
by A1, FINSEQ_1:17;
then A9:
rng G c= the carrier of L
by TARSKI:def 3;
hence
G1 is FinSequence of L
by FINSEQ_1:def 4; ( dom G1 c= dom F & len G1 = k & F = G1 ^ <*(F /. (k + 1))*> )
reconsider G = G as FinSequence of L by A9, FINSEQ_1:def 4;
A10: dom (G ^ <*(F /. (k + 1))*>) =
Seg ((len G) + (len <*(F /. (k + 1))*>))
by FINSEQ_1:def 7
.=
Seg (k + 1)
by A4, FINSEQ_1:40
.=
dom F
by A2, FINSEQ_1:def 3
;
hence
dom G1 c= dom F
by FINSEQ_1:26; ( len G1 = k & F = G1 ^ <*(F /. (k + 1))*> )
thus
len G1 = k
by A1, A3, FINSEQ_1:17; F = G1 ^ <*(F /. (k + 1))*>
now for j being Nat st j in dom F holds
F . j = (G ^ <*(F /. (k + 1))*>) . jlet j be
Nat;
( j in dom F implies F . b1 = (G ^ <*(F /. (k + 1))*>) . b1 )assume A11:
j in dom F
;
F . b1 = (G ^ <*(F /. (k + 1))*>) . b1per cases
( j in dom G or not j in dom G )
;
suppose A13:
not
j in dom G
;
(G ^ <*(F /. (k + 1))*>) . b1 = F . b1A14:
dom F = Seg (len F)
by FINSEQ_1:def 3;
then A15:
1
<= j
by A11, FINSEQ_1:1;
A16:
now not j < k + 1end;
j <= k + 1
by A2, A11, A14, FINSEQ_1:1;
then A17:
j = k + 1
by A16, XXREAL_0:1;
dom <*(F /. (k + 1))*> = {1}
by FINSEQ_1:2, FINSEQ_1:38;
then
1
in dom <*(F /. (k + 1))*>
by TARSKI:def 1;
hence (G ^ <*(F /. (k + 1))*>) . j =
<*(F /. (k + 1))*> . 1
by A4, A17, FINSEQ_1:def 7
.=
F /. (k + 1)
by FINSEQ_1:40
.=
F . j
by A11, A17, PARTFUN1:def 6
;
verum end; end; end;
hence
F = G1 ^ <*(F /. (k + 1))*>
by A10, FINSEQ_1:13; verum