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 A1: ( G1 = F | (Seg k) & 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 ;
A2: k <= len F by A1, NAT_1:13;
then A3: len G = k by A1, FINSEQ_1:21;

now

let u be set ; :: 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 set such that
A4: ( x in dom G & G . x = u ) by FUNCT_1:def 5;
reconsider x' = x as Element of NAT by A4;
A5: ( 1 <= x' & x' <= len G ) by A4, FINSEQ_3:27;
then x' <= len F by A1, A3, NAT_1:12;
then A6: x in dom F by A5, FINSEQ_3:27;
G . x = F . x by A1, A4, FUNCT_1:70
.= F /. x by A6, PARTFUN1:def 8 ;
hence u in the carrier of L by A4; :: thesis: verum

end;

then A7: rng G c= the carrier of L by TARSKI:def 3;
then reconsider G = G as FinSequence of L by FINSEQ_1:def 4;
thus G1 is FinSequence of L by A7, FINSEQ_1:def 4; :: thesis: ( dom G1 c= dom F & len G1 = k & F = G1 ^ <*(F /. (k + 1))*> )
A8: dom (G ^ <*(F /. (k + 1))*>) = Seg ((len G) + (len <*(F /. (k + 1))*>)) by FINSEQ_1:def 7
.= Seg (k + 1) by A3, FINSEQ_1:57
.= dom F by A1, FINSEQ_1:def 3 ;
hence dom G1 c= dom F by FINSEQ_1:39; :: thesis: ( len G1 = k & F = G1 ^ <*(F /. (k + 1))*> )
thus len G1 = k by A1, A2, FINSEQ_1:21; :: thesis: F = G1 ^ <*(F /. (k + 1))*>

now

let j be Nat; :: thesis: ( j in dom F implies F . b₁ = (G ^ <*(F /. (k + 1))*>) . b₁ )
assume A9: 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 A10: j in dom G ; :: thesis: F . b₁ = (G ^ <*(F /. (k + 1))*>) . b₁

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

end;

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

A12: j = k + 1

proof

dom F = Seg (len F) by FINSEQ_1:def 3;
then A13: ( 1 <= j & j <= k + 1 ) by A1, A9, FINSEQ_1:3;

now

assume j < k + 1 ; :: thesis: contradiction
then j <= k by NAT_1:13;
then j in Seg k by A9, A13;
hence contradiction by A1, A2, A11, FINSEQ_1:21; :: thesis: verum

end;

hence j = k + 1 by A13, XXREAL_0:1; :: thesis: verum

end;

dom <*(F /. (k + 1))*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then 1 in dom <*(F /. (k + 1))*> by TARSKI:def 1;
hence (G ^ <*(F /. (k + 1))*>) . j = <*(F /. (k + 1))*> . 1 by A3, A12, FINSEQ_1:def 7
.= F /. (k + 1) by FINSEQ_1:57
.= F . j by A9, A12, PARTFUN1:def 8 ;
:: thesis: verum

end;

end;

end;

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