let m, n, k be non zero Nat; :: thesis: for X being non-empty m -element FinSequence st k <= n & n <= m holds
SubFin (X,k) = SubFin ((SubFin (X,n)),k)
let X be non-empty m -element FinSequence; :: thesis: ( k <= n & n <= m implies SubFin (X,k) = SubFin ((SubFin (X,n)),k) )
assume that
A1: k <= n and
A2: n <= m ; :: thesis: SubFin (X,k) = SubFin ((SubFin (X,n)),k)
A3: SubFin (X,n) = X | n by A2, Def5;
A4: SubFin ((SubFin (X,n)),k) = (X | n) | k by A1, A3, Def5;
SubFin (X,k) = X | k by A2, A1, XXREAL_0:2, Def5;
hence SubFin (X,k) = SubFin ((SubFin (X,n)),k) by A4, A1, FINSEQ_1:82; :: thesis: verum