let S, T be Polish-language; :: thesis: for u being FinSequence st u in S ^ T holds
( S -head u in S & S -tail u in T )
let u be FinSequence; :: thesis: ( u in S ^ T implies ( S -head u in S & S -tail u in T ) )
assume u in S ^ T ; :: thesis: ( S -head u in S & S -tail u in T )
then consider s, t being FinSequence such that
A2: ( u = s ^ t & s in S & t in T ) by Def2;
thus ( S -head u in S & S -tail u in T ) by A2, Th52; :: thesis: verum