let p be FinSequence; :: thesis: for k1, k2 being Nat st k1 < k2 & k1 in dom p holds
mid (p,k1,k2) = <*(p . k1)*> ^ (mid (p,(k1 + 1),k2))
let k1, k2 be Nat; :: thesis: ( k1 < k2 & k1 in dom p implies mid (p,k1,k2) = <*(p . k1)*> ^ (mid (p,(k1 + 1),k2)) )
assume A1: ( k1 < k2 & k1 in dom p ) ; :: thesis: mid (p,k1,k2) = <*(p . k1)*> ^ (mid (p,(k1 + 1),k2))
then reconsider D = rng p as non empty set by FUNCT_1:3;
reconsider q = p as FinSequence of D by FINSEQ_1:def 4;
mid (q,k1,k2) = <*(q . k1)*> ^ (mid (q,(k1 + 1),k2)) by A1, Th126;
hence mid (p,k1,k2) = <*(p . k1)*> ^ (mid (p,(k1 + 1),k2)) ; :: thesis: verum