let m, n1, n2, k be non zero Nat; :: thesis: for X being non-empty m -element FinSequence st k <= n1 & n1 <= n2 & n2 <= m holds
( SubFin ((SubFin (X,n1)),k) = SubFin ((SubFin (X,n2)),k) & ElmFin ((SubFin (X,n1)),k) = ElmFin ((SubFin (X,n2)),k) )
let X be non-empty m -element FinSequence; :: thesis: ( k <= n1 & n1 <= n2 & n2 <= m implies ( SubFin ((SubFin (X,n1)),k) = SubFin ((SubFin (X,n2)),k) & ElmFin ((SubFin (X,n1)),k) = ElmFin ((SubFin (X,n2)),k) ) )
assume that
A1: k <= n1 and
A2: n1 <= n2 and
A3: n2 <= m ; :: thesis: ( SubFin ((SubFin (X,n1)),k) = SubFin ((SubFin (X,n2)),k) & ElmFin ((SubFin (X,n1)),k) = ElmFin ((SubFin (X,n2)),k) )
A4: ( SubFin (X,n1) = X | n1 & SubFin (X,n2) = X | n2 ) by A2, A3, XXREAL_0:2, MEASUR13:def 5;
then A5: SubFin ((SubFin (X,n2)),k) = (X | n2) | k by A1, A2, XXREAL_0:2, MEASUR13:def 5;
A6: k <= n2 by A1, A2, XXREAL_0:2;
then ( (X | n1) | k = X | k & (X | n2) | k = X | k ) by A1, FINSEQ_1:5, RELAT_1:74;
hence SubFin ((SubFin (X,n1)),k) = SubFin ((SubFin (X,n2)),k) by A5, A1, A4, MEASUR13:def 5; :: thesis: ElmFin ((SubFin (X,n1)),k) = ElmFin ((SubFin (X,n2)),k)
1 <= k by NAT_1:14;
then A7: ( k in Seg n1 & k in Seg n2 ) by A1, A6;
( ElmFin ((SubFin (X,n1)),k) = (X | n1) . k & ElmFin ((SubFin (X,n2)),k) = (X | n2) . k ) by A1, A4, A2, XXREAL_0:2, MEASUR13:def 1;
then ( ElmFin ((SubFin (X,n1)),k) = X . k & ElmFin ((SubFin (X,n2)),k) = X . k ) by A7, FUNCT_1:49;
hence ElmFin ((SubFin (X,n1)),k) = ElmFin ((SubFin (X,n2)),k) ; :: thesis: verum