let U be non empty set ; :: thesis: for x, y being FinSequence st x is U -valued & y is U -valued holds
(U -concatenation) . (x,y) = x ^ y
let x, y be FinSequence; :: thesis: ( x is U -valued & y is U -valued implies (U -concatenation) . (x,y) = x ^ y )
set f = U -concatenation ;
assume ( x is U -valued & y is U -valued ) ; :: thesis: (U -concatenation) . (x,y) = x ^ y
then reconsider xx = x, yy = y as FinSequence of U by Lm1;
(U -concatenation) . (xx,yy) = xx ^ yy by Lm10;
hence (U -concatenation) . (x,y) = x ^ y ; :: thesis: verum