let p be FuncSequence; :: thesis: for f being Function st lastrng p c= dom f holds
p ^ <*f*> is FuncSequence
let f be Function; :: thesis: ( lastrng p c= dom f implies p ^ <*f*> is FuncSequence )
assume A1: lastrng p c= dom f ; :: thesis: p ^ <*f*> is FuncSequence
consider q being FinSequence such that
A2: len q = (len p) + 1 and
A3: for i being Nat st i in dom p holds
p . i in Funcs ((q . i),(q . (i + 1))) by Def7;
consider q9 being FinSequence, x being object such that
A4: q = q9 ^ <*x*> by A2, CARD_1:27, FINSEQ_1:46;

A5: now :: thesis: ( len p in dom p implies p . (len p) in Funcs ((q . (len p)),(dom f)) )

assume A6: len p in dom p ; :: thesis: p . (len p) in Funcs ((q . (len p)),(dom f))
then p . (len p) in Funcs ((q . (len p)),(q . ((len p) + 1))) by A3;
then consider g being Function such that
A7: p . (len p) = g and
A8: dom g = q . (len p) and
rng g c= q . ((len p) + 1) by FUNCT_2:def 2;
lastrng p = rng g by A6, A7, Def6, RELAT_1:38;
hence p . (len p) in Funcs ((q . (len p)),(dom f)) by A1, A7, A8, FUNCT_2:def 2; :: thesis: verum

end;

A9: <*(dom f),(rng f)*> . 1 = dom f ;
A10: <*(dom f),(rng f)*> . 2 = rng f ;
len <*f*> = 1 by FINSEQ_1:40;
then A11: len (p ^ <*f*>) = (len p) + 1 by FINSEQ_1:22;
set r = q9 ^ <*(dom f),(rng f)*>;
len <*(dom f),(rng f)*> = 2 by FINSEQ_1:44;
then A12: len (q9 ^ <*(dom f),(rng f)*>) = (len q9) + (1 + 1) by FINSEQ_1:22;
A13: dom <*(dom f),(rng f)*> = Seg 2 by FINSEQ_1:89;
then A14: 1 in dom <*(dom f),(rng f)*> by FINSEQ_1:2, TARSKI:def 2;
len <*x*> = 1 by FINSEQ_1:40;
then A15: len q = (len q9) + 1 by A4, FINSEQ_1:22;
A16: 2 in dom <*(dom f),(rng f)*> by A13, FINSEQ_1:2, TARSKI:def 2;
p ^ <*f*> is FuncSeq-like

proof

take q9 ^ <*(dom f),(rng f)*> ; :: according to FUNCT_7:def 8 :: thesis: ( len (q9 ^ <*(dom f),(rng f)*>) = (len (p ^ <*f*>)) + 1 & ( for i being Nat st i in dom (p ^ <*f*>) holds
(p ^ <*f*>) . i in Funcs (((q9 ^ <*(dom f),(rng f)*>) . i),((q9 ^ <*(dom f),(rng f)*>) . (i + 1))) ) )
thus len (q9 ^ <*(dom f),(rng f)*>) = (len (p ^ <*f*>)) + 1 by A2, A15, A11, A12; :: thesis: for i being Nat st i in dom (p ^ <*f*>) holds
(p ^ <*f*>) . i in Funcs (((q9 ^ <*(dom f),(rng f)*>) . i),((q9 ^ <*(dom f),(rng f)*>) . (i + 1)))
let i be Nat; :: thesis: ( i in dom (p ^ <*f*>) implies (p ^ <*f*>) . i in Funcs (((q9 ^ <*(dom f),(rng f)*>) . i),((q9 ^ <*(dom f),(rng f)*>) . (i + 1))) )
assume A17: i in dom (p ^ <*f*>) ; :: thesis: (p ^ <*f*>) . i in Funcs (((q9 ^ <*(dom f),(rng f)*>) . i),((q9 ^ <*(dom f),(rng f)*>) . (i + 1)))
then A18: i >= 1 by FINSEQ_3:25;
i <= (len p) + 1 by A11, A17, FINSEQ_3:25;
then A19: ( i = (len p) + 1 or len p >= i ) by NAT_1:8;

per cases ( i = (len p) + 1 or i = len p or i < len p ) by A19, XXREAL_0:1;

suppose A20: i = (len p) + 1 ; :: thesis: (p ^ <*f*>) . i in Funcs (((q9 ^ <*(dom f),(rng f)*>) . i),((q9 ^ <*(dom f),(rng f)*>) . (i + 1)))

then A21: ( (q9 ^ <*(dom f),(rng f)*>) . i = dom f & (p ^ <*f*>) . i = f ) by A2, A15, A14, A9, FINSEQ_1:42, FINSEQ_1:def 7;
(q9 ^ <*(dom f),(rng f)*>) . (i + 1) = rng f by A2, A15, A12, A16, A10, A20, FINSEQ_1:def 7;
hence (p ^ <*f*>) . i in Funcs (((q9 ^ <*(dom f),(rng f)*>) . i),((q9 ^ <*(dom f),(rng f)*>) . (i + 1))) by A21, FUNCT_2:def 2; :: thesis: verum

end;

suppose A22: i = len p ; :: thesis: (p ^ <*f*>) . i in Funcs (((q9 ^ <*(dom f),(rng f)*>) . i),((q9 ^ <*(dom f),(rng f)*>) . (i + 1)))

then i in dom q9 by A2, A15, A18, FINSEQ_3:25;
then A23: ( (q9 ^ <*(dom f),(rng f)*>) . i = q9 . i & q9 . i = q . i ) by A4, FINSEQ_1:def 7;
( len p in dom p & (q9 ^ <*(dom f),(rng f)*>) . (i + 1) = dom f ) by A2, A15, A14, A9, A18, A22, FINSEQ_1:def 7, FINSEQ_3:25;
hence (p ^ <*f*>) . i in Funcs (((q9 ^ <*(dom f),(rng f)*>) . i),((q9 ^ <*(dom f),(rng f)*>) . (i + 1))) by A5, A22, A23, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A24: i < len p ; :: thesis: (p ^ <*f*>) . i in Funcs (((q9 ^ <*(dom f),(rng f)*>) . i),((q9 ^ <*(dom f),(rng f)*>) . (i + 1)))

then i in dom q9 by A2, A15, A18, FINSEQ_3:25;
then A25: ( q . i = q9 . i & q9 . i = (q9 ^ <*(dom f),(rng f)*>) . i ) by A4, FINSEQ_1:def 7;
A26: i + 1 >= 1 by NAT_1:11;
i in dom p by A18, A24, FINSEQ_3:25;
then A27: ( p . i in Funcs ((q . i),(q . (i + 1))) & p . i = (p ^ <*f*>) . i ) by A3, FINSEQ_1:def 7;
i + 1 <= len p by A24, NAT_1:13;
then A28: i + 1 in dom q9 by A2, A15, A26, FINSEQ_3:25;
then q . (i + 1) = q9 . (i + 1) by A4, FINSEQ_1:def 7;
hence (p ^ <*f*>) . i in Funcs (((q9 ^ <*(dom f),(rng f)*>) . i),((q9 ^ <*(dom f),(rng f)*>) . (i + 1))) by A28, A25, A27, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

hence p ^ <*f*> is FuncSequence ; :: thesis: verum