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 Element of NAT st i in dom p holds
p . i in Funcs (q . i),(q . (i + 1)) by Def8;
consider q' being FinSequence, x being set such that
A4: q = q' ^ <*x*> by A2, CARD_1:47, FINSEQ_1:63;
set r = q' ^ <*(dom f),(rng f)*>;
( len <*(dom f),(rng f)*> = 2 & len <*f*> = 1 & len <*x*> = 1 ) by FINSEQ_1:57, FINSEQ_1:61;
then A5: ( len q = (len q') + 1 & len (p ^ <*f*>) = (len p) + 1 & len (q' ^ <*(dom f),(rng f)*>) = (len q') + (1 + 1) ) by A4, FINSEQ_1:35;
dom <*(dom f),(rng f)*> = Seg 2 by FINSEQ_3:29;
then A6: ( 1 in dom <*(dom f),(rng f)*> & 2 in dom <*(dom f),(rng f)*> & <*(dom f),(rng f)*> . 1 = dom f & <*(dom f),(rng f)*> . 2 = rng f ) by FINSEQ_1:4, FINSEQ_1:61, TARSKI:def 2;

A7: now

assume A8: 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
A9: ( p . (len p) = g & dom g = q . (len p) & rng g c= q . ((len p) + 1) ) by FUNCT_2:def 2;
lastrng p = rng g by A9, Def7, A8, RELAT_1:60;
hence p . (len p) in Funcs (q . (len p)),(dom f) by A1, A9, FUNCT_2:def 2; :: thesis: verum

end;

p ^ <*f*> is FuncSeq-like

proof

take q' ^ <*(dom f),(rng f)*> ; :: according to FUNCT_7:def 8 :: thesis: ( len (q' ^ <*(dom f),(rng f)*>) = (len (p ^ <*f*>)) + 1 & ( for i being Element of NAT st i in dom (p ^ <*f*>) holds
(p ^ <*f*>) . i in Funcs ((q' ^ <*(dom f),(rng f)*>) . i),((q' ^ <*(dom f),(rng f)*>) . (i + 1)) ) )
thus len (q' ^ <*(dom f),(rng f)*>) = (len (p ^ <*f*>)) + 1 by A2, A5; :: thesis: for i being Element of NAT st i in dom (p ^ <*f*>) holds
(p ^ <*f*>) . i in Funcs ((q' ^ <*(dom f),(rng f)*>) . i),((q' ^ <*(dom f),(rng f)*>) . (i + 1))
let i be Element of NAT ; :: thesis: ( i in dom (p ^ <*f*>) implies (p ^ <*f*>) . i in Funcs ((q' ^ <*(dom f),(rng f)*>) . i),((q' ^ <*(dom f),(rng f)*>) . (i + 1)) )
assume i in dom (p ^ <*f*>) ; :: thesis: (p ^ <*f*>) . i in Funcs ((q' ^ <*(dom f),(rng f)*>) . i),((q' ^ <*(dom f),(rng f)*>) . (i + 1))
then A10: ( i <= (len p) + 1 & i >= 1 ) by A5, FINSEQ_3:27;
then A11: ( 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 A11, XXREAL_0:1;

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

then ( (q' ^ <*(dom f),(rng f)*>) . i = dom f & (p ^ <*f*>) . i = f & (q' ^ <*(dom f),(rng f)*>) . (i + 1) = rng f ) by A2, A5, A6, FINSEQ_1:59, FINSEQ_1:def 7;
hence (p ^ <*f*>) . i in Funcs ((q' ^ <*(dom f),(rng f)*>) . i),((q' ^ <*(dom f),(rng f)*>) . (i + 1)) by FUNCT_2:def 2; :: thesis: verum

end;

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

then ( len p in dom p & i in dom q' ) by A2, A5, A10, FINSEQ_3:27;
then ( p . i in Funcs (q . i),(dom f) & (q' ^ <*(dom f),(rng f)*>) . (i + 1) = dom f & (q' ^ <*(dom f),(rng f)*>) . i = q' . i & q' . i = q . i & (p ^ <*f*>) . i = p . i ) by A2, A4, A5, A6, A7, A12, FINSEQ_1:def 7;
hence (p ^ <*f*>) . i in Funcs ((q' ^ <*(dom f),(rng f)*>) . i),((q' ^ <*(dom f),(rng f)*>) . (i + 1)) ; :: thesis: verum

end;

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

then ( i <= len p & i + 1 <= len p & i + 1 >= 1 ) by NAT_1:11, NAT_1:13;
then ( i in dom p & i in dom q' & i + 1 in dom q' ) by A2, A5, A10, FINSEQ_3:27;
then ( p . i in Funcs (q . i),(q . (i + 1)) & q . i = q' . i & q' . i = (q' ^ <*(dom f),(rng f)*>) . i & p . i = (p ^ <*f*>) . i & q . (i + 1) = q' . (i + 1) & q' . (i + 1) = (q' ^ <*(dom f),(rng f)*>) . (i + 1) ) by A3, A4, FINSEQ_1:def 7;
hence (p ^ <*f*>) . i in Funcs ((q' ^ <*(dom f),(rng f)*>) . i),((q' ^ <*(dom f),(rng f)*>) . (i + 1)) ; :: thesis: verum

end;

end;

end;

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