reconsider pp = p, qq = q as FinSequence of U by Lm1;
pp ^ qq is U -valued ;
hence for b₁ being FinSequence st b₁ = p ^ q holds
b₁ is U -valued ; :: thesis: verum