theorem Th4: :: FOMODEL0:4

for U being non empty set
for x, y being FinSequence st x is U -valued & y is U -valued holds
(U -concatenation) . (x,y) = x ^ y