let p, q be FinSequence; :: thesis: for x, y being object holds (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q
let x, y be object ; :: thesis: (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q
(p ^ <*y*>) ^ q = p ^ (<*y*> ^ q) by FINSEQ_1:32;
hence (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q by Th2; :: thesis: verum