let q be FinSequence; :: thesis: for x being object st q <> {} holds
<*x*> $^ q = q
let x be object ; :: thesis: ( q <> {} implies <*x*> $^ q = q )
( {} ^ <*x*> = <*x*> & {} ^ q = q ) by FINSEQ_1:34;
hence ( q <> {} implies <*x*> $^ q = q ) by Th2; :: thesis: verum