let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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;

now :: thesis: for u being object st u in rng G holds
u in the carrier of L

let u be object ; :: thesis: ( u in rng G implies u in the carrier of L )
assume u in rng G ; :: thesis: u in the carrier of L
then consider x being object such that
A5: x in dom G and
A6: G . x = u by FUNCT_1:def 3;
reconsider x9 = x as Element of NAT by A5;
x9 <= len G by A5, FINSEQ_3:25;
then A7: x9 <= len F by A2, A4, NAT_1:12;
1 <= x9 by A5, FINSEQ_3:25;
then A8: x in dom F by A7, FINSEQ_3:25;
G . x = F . x by A1, A5, FUNCT_1:47
.= F /. x by A8, PARTFUN1:def 6 ;
hence u in the carrier of L by A6; :: thesis: verum

end;

then A9: rng G c= the carrier of L by TARSKI:def 3;
hence G1 is FinSequence of L by FINSEQ_1:def 4; :: thesis: ( 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; :: thesis: ( len G1 = k & F = G1 ^ <*(F /. (k + 1))*> )
thus len G1 = k by A1, A3, FINSEQ_1:17; :: thesis: F = G1 ^ <*(F /. (k + 1))*>

now :: thesis: for j being Nat st j in dom F holds
F . j = (G ^ <*(F /. (k + 1))*>) . j

let j be Nat; :: thesis: ( j in dom F implies F . b₁ = (G ^ <*(F /. (k + 1))*>) . b₁ )
assume A11: j in dom F ; :: thesis: F . b₁ = (G ^ <*(F /. (k + 1))*>) . b₁

per cases ( j in dom G or not j in dom G ) ;

suppose A12: j in dom G ; :: thesis: F . b₁ = (G ^ <*(F /. (k + 1))*>) . b₁

hence F . j = G . j by A1, FUNCT_1:47
.= (G ^ <*(F /. (k + 1))*>) . j by A12, FINSEQ_1:def 7 ;
:: thesis: verum

end;

suppose A13: not j in dom G ; :: thesis: (G ^ <*(F /. (k + 1))*>) . b₁ = F . b₁

A14: dom F = Seg (len F) by FINSEQ_1:def 3;
then A15: 1 <= j by A11, FINSEQ_1:1;

A16: now :: thesis: not j < k + 1

assume j < k + 1 ; :: thesis: contradiction
then j <= k by NAT_1:13;
then j in Seg k by A15;
hence contradiction by A1, A3, A13, FINSEQ_1:17; :: thesis: verum

end;

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)
.= F . j by A11, A17, PARTFUN1:def 6 ;
:: thesis: verum

end;

end;

end;

hence F = G1 ^ <*(F /. (k + 1))*> by A10, FINSEQ_1:13; :: thesis: verum