defpred S₁[ set , set , set ] means ex a being adjective of T st
( a = p . $1 & ( ( $2 is not type of T & $3 = 0 ) or ex t being type of T st
( t = $2 & $3 = a ast t ) ) );
A1: for i being Nat st 1 <= i & i < (len p) + 1 holds
for x being set ex y being set st S₁[i,x,y]

proof

let i be Nat; :: thesis: ( 1 <= i & i < (len p) + 1 implies for x being set ex y being set st S₁[i,x,y] )
assume A2: 1 <= i ; :: thesis: ( not i < (len p) + 1 or for x being set ex y being set st S₁[i,x,y] )
assume i < (len p) + 1 ; :: thesis: for x being set ex y being set st S₁[i,x,y]
then i <= len p by NAT_1:13;
then i in dom p by A2, FINSEQ_3:25;
then p . i in rng p by FUNCT_1:3;
then reconsider a = p . i as adjective of T ;
let x be set ; :: thesis: ex y being set st S₁[i,x,y]

per cases ( not x is type of T or x is type of T ) ;

suppose A3: x is not type of T ; :: thesis: ex y being set st S₁[i,x,y]

take 0 ; :: thesis: S₁[i,x, 0 ]
take a ; :: thesis: ( a = p . i & ( ( x is not type of T & 0 = 0 ) or ex t being type of T st
( t = x & 0 = a ast t ) ) )
thus ( a = p . i & ( ( x is not type of T & 0 = 0 ) or ex t being type of T st
( t = x & 0 = a ast t ) ) ) by A3; :: thesis: verum

end;

suppose x is type of T ; :: thesis: ex y being set st S₁[i,x,y]

then reconsider t = x as type of T ;
take a ast t ; :: thesis: S₁[i,x,a ast t]
take a ; :: thesis: ( a = p . i & ( ( x is not type of T & a ast t = 0 ) or ex t being type of T st
( t = x & a ast t = a ast t ) ) )
thus a = p . i ; :: thesis: ( ( x is not type of T & a ast t = 0 ) or ex t being type of T st
( t = x & a ast t = a ast t ) )
thus ( ( x is not type of T & a ast t = 0 ) or ex t being type of T st
( t = x & a ast t = a ast t ) ) ; :: thesis: verum

end;

end;

end;

consider q being FinSequence such that
A4: len q = (len p) + 1 and
A5: ( q . 1 = t or (len p) + 1 = 0 ) and
A6: for i being Nat st 1 <= i & i < (len p) + 1 holds
S₁[i,q . i,q . (i + 1)] from RECDEF_1:sch 3(A1);
defpred S₂[ Nat] means ( $1 in dom q implies q . $1 is type of T );

A7: now :: thesis: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A8: S₂[k] ; :: thesis: S₂[k + 1]

now :: thesis: ( k + 1 in dom q implies q . (k + 1) is type of T )

assume k + 1 in dom q ; :: thesis: q . (k + 1) is type of T
then k + 1 <= len q by FINSEQ_3:25;
then A9: k < len q by NAT_1:13;
A10: ( k <> 0 implies k >= 0 + 1 ) by NAT_1:13;
then ( k <> 0 implies ex a being adjective of T st
( a = p . k & ( ( q . k is not type of T & q . (k + 1) = 0 ) or ex t being type of T st
( t = q . k & q . (k + 1) = a ast t ) ) ) ) by A4, A6, A9;
hence q . (k + 1) is type of T by A5, A8, A10, A9, FINSEQ_3:25; :: thesis: verum

end;

hence S₂[k + 1] ; :: thesis: verum

end;

A11: S₂[ 0 ] by FINSEQ_3:24;
A12: for k being Nat holds S₂[k] from NAT_1:sch 2(A11, A7);
rng q c= the carrier of T

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng q or a in the carrier of T )
assume a in rng q ; :: thesis: a in the carrier of T
then ex x being object st
( x in dom q & a = q . x ) by FUNCT_1:def 3;
then a is type of T by A12;
hence a in the carrier of T ; :: thesis: verum

end;

then reconsider q = q as FinSequence of the carrier of T by FINSEQ_1:def 4;
take q ; :: thesis: ( len q = (len p) + 1 & q . 1 = t & ( for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = q . i holds
q . (i + 1) = a ast t ) )
thus ( len q = (len p) + 1 & q . 1 = t ) by A4, A5; :: thesis: for i being Element of NAT
for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = q . i holds
q . (i + 1) = a ast t
let i be Element of NAT ; :: thesis: for a being adjective of T
for t being type of T st i in dom p & a = p . i & t = q . i holds
q . (i + 1) = a ast t
let a be adjective of T; :: thesis: for t being type of T st i in dom p & a = p . i & t = q . i holds
q . (i + 1) = a ast t
let t be type of T; :: thesis: ( i in dom p & a = p . i & t = q . i implies q . (i + 1) = a ast t )
assume that
A13: i in dom p and
A14: a = p . i and
A15: t = q . i ; :: thesis: q . (i + 1) = a ast t
i <= len p by A13, FINSEQ_3:25;
then A16: i < (len p) + 1 by NAT_1:13;
i >= 1 by A13, FINSEQ_3:25;
then ex a being adjective of T st
( a = p . i & ( ( q . i is not type of T & q . (i + 1) = 0 ) or ex t being type of T st
( t = q . i & q . (i + 1) = a ast t ) ) ) by A6, A16;
hence q . (i + 1) = a ast t by A14, A15; :: thesis: verum