take q = <*(dom f),(rng f)*>; :: according to FUNCT_7:def 8 :: thesis: ( len q = (len <*f*>) + 1 & ( for i being Element of NAT st i in dom <*f*> holds
<*f*> . i in Funcs (q . i),(q . (i + 1)) ) )
set p = <*f*>;
thus len q = 1 + 1 by FINSEQ_1:61
.= (len <*f*>) + 1 by FINSEQ_1:57 ; :: thesis: for i being Element of NAT st i in dom <*f*> holds
<*f*> . i in Funcs (q . i),(q . (i + 1))
let i be Element of NAT ; :: thesis: ( i in dom <*f*> implies <*f*> . i in Funcs (q . i),(q . (i + 1)) )
assume i in dom <*f*> ; :: thesis: <*f*> . i in Funcs (q . i),(q . (i + 1))
then i in {1} by FINSEQ_1:4, FINSEQ_1:55;
then A1: i = 1 by TARSKI:def 1;
then A2: q . (i + 1) = rng f by FINSEQ_1:61;
( <*f*> . i = f & q . i = dom f ) by A1, FINSEQ_1:57, FINSEQ_1:61;
hence <*f*> . i in Funcs (q . i),(q . (i + 1)) by A2, FUNCT_2:def 2; :: thesis: verum