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 Element of 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 Element of 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:27;
then ( p . i in rng p & rng p c= the adjectives of T ) by FUNCT_1:12;
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
A5: len q = (len p) + 1 and
A6: ( q . 1 = t or (len p) + 1 = 0 ) and
A7: for i being Element of NAT st 1 <= i & i < (len p) + 1 holds
S₁[i,q . i,q . (i + 1)] from RECDEF_1:sch 3(A1);
defpred S₂[ Element of NAT ] means ( $1 in dom q implies q . $1 is type of T );
A8: S₂[ 0 ] by FINSEQ_3:26;

A9: now

let k be Element of NAT ; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A10: S₂[k] ; :: thesis: S₂[k + 1]

now

assume k + 1 in dom q ; :: thesis: q . (k + 1) is type of T
then ( ( k <> 0 implies k > 0 ) & k + 1 <= len q ) by FINSEQ_3:27;
then A11: ( ( k <> 0 implies k >= 0 + 1 ) & k < len q ) 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 A5, A7;
hence q . (k + 1) is type of T by A6, A10, A11, FINSEQ_3:27; :: thesis: verum

end;

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

end;

A12: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A8, A9);
rng q c= the carrier of T

proof

let a be set ; :: 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 consider x being set such that
A13: ( x in dom q & a = q . x ) by FUNCT_1:def 5;
a is type of T by A12, A13;
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 A5, A6; :: 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 A14: ( i in dom p & a = p . i & t = q . i ) ; :: thesis: q . (i + 1) = a ast t
then ( i >= 1 & i <= len p ) by FINSEQ_3:27;
then ( i >= 1 & i < (len p) + 1 ) by NAT_1:13;
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 A7;
hence q . (i + 1) = a ast t by A14; :: thesis: verum