take q = <*(dom f),(rng f)*>; :: according to FUNCT_7:def 8 :: thesis: ( len q = (len <*f*>) + 1 & ( for i being 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:44
.= (len <*f*>) + 1 by FINSEQ_1:40 ; :: thesis: for i being Nat st i in dom <*f*> holds
<*f*> . i in Funcs ((q . i),(q . (i + 1)))
let i be 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:2, FINSEQ_1:38;
then A1: i = 1 by TARSKI:def 1;
then A2: q . (i + 1) = rng f ;
( <*f*> . i = f & q . i = dom f ) by A1;
hence <*f*> . i in Funcs ((q . i),(q . (i + 1))) by A2, FUNCT_2:def 2; :: thesis: verum