let f, g be FinSequence; :: thesis: f | (Seg 0 ) = g | (Seg 0 )
f | (Seg 0 ) = {} by Th4;
hence f | (Seg 0 ) = g | (Seg 0 ) by Th4; :: thesis: verum