let m, n, k be non zero Nat; :: thesis: for X being non-empty m -element FinSequence st k <= n & n <= m holds
ElmFin (X,k) = ElmFin ((SubFin (X,n)),k)
let X be non-empty m -element FinSequence; :: thesis: ( k <= n & n <= m implies ElmFin (X,k) = ElmFin ((SubFin (X,n)),k) )
assume that
A1: k <= n and
A2: n <= m ; :: thesis: ElmFin (X,k) = ElmFin ((SubFin (X,n)),k)
A3: ElmFin (X,k) = X . k by A1, A2, Def1, XXREAL_0:2;
1 <= k by NAT_1:14;
then A4: k in Seg n by A1;
SubFin (X,n) = X | n by A2, Def5;
then ElmFin ((SubFin (X,n)),k) = (X | n) . k by A1, Def1;
hence ElmFin (X,k) = ElmFin ((SubFin (X,n)),k) by A3, A4, FUNCT_1:49; :: thesis: verum