let U be non empty set ; :: thesis: for p being FinSequence st p is U -valued & not p is empty holds
(U -firstChar) . p = p . 1
let p be FinSequence; :: thesis: ( p is U -valued & not p is empty implies (U -firstChar) . p = p . 1 )
assume ( p is U -valued & not p is empty ) ; :: thesis: (U -firstChar) . p = p . 1
then reconsider pp = p as non empty FinSequence of U by Lm1;
(U -firstChar) . pp = pp . 1 by Lm22;
hence (U -firstChar) . p = p . 1 ; :: thesis: verum