let q1, q2 be FinSequence of the carrier of T; :: thesis: ( len q1 = (len p) + 1 & q1 . 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 = q1 . i holds
q1 . (i + 1) = a ast t ) & len q2 = (len p) + 1 & q2 . 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 = q2 . i holds
q2 . (i + 1) = a ast t ) implies q1 = q2 )
assume that
A17: len q1 = (len p) + 1 and
A18: q1 . 1 = t and
A19: 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 = q1 . i holds
q1 . (i + 1) = a ast t and
A20: len q2 = (len p) + 1 and
A21: q2 . 1 = t and
A22: 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 = q2 . i holds
q2 . (i + 1) = a ast t ; :: thesis: q1 = q2
defpred S₁[ Nat] means ( $1 in dom q1 implies q1 . $1 = q2 . $1 );

A23: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A24: S₁[i] ; :: thesis: S₁[i + 1]

now :: thesis: ( i + 1 in dom q1 implies q1 . (i + 1) = q2 . (i + 1) )

assume i + 1 in dom q1 ; :: thesis: q1 . (i + 1) = q2 . (i + 1)
then A25: i + 1 <= len q1 by FINSEQ_3:25;
then A26: i <= len q1 by NAT_1:13;
A27: i <= len p by A17, A25, XREAL_1:6;

per cases ( i = 0 or i > 0 ) ;

suppose i = 0 ; :: thesis: q1 . (i + 1) = q2 . (i + 1)

hence q1 . (i + 1) = q2 . (i + 1) by A18, A21; :: thesis: verum

end;

suppose i > 0 ; :: thesis: q1 . (i + 1) = q2 . (i + 1)

then A28: i >= 0 + 1 by NAT_1:13;
then A29: i in dom p by A27, FINSEQ_3:25;
then reconsider a = p . i as adjective of T by FINSEQ_2:11;
i in dom q1 by A26, A28, FINSEQ_3:25;
then reconsider t = q1 . i as type of T by FINSEQ_2:11;
thus q1 . (i + 1) = a ast t by A19, A29
.= q2 . (i + 1) by A22, A24, A26, A28, A29, FINSEQ_3:25 ; :: thesis: verum

end;

end;

end;

hence S₁[i + 1] ; :: thesis: verum

end;

A30: S₁[ 0 ] by FINSEQ_3:25;
A31: for i being Nat holds S₁[i] from NAT_1:sch 2(A30, A23);
dom q1 = dom q2 by A17, A20, FINSEQ_3:29;
hence q1 = q2 by A31; :: thesis: verum