let p, q be FinSequence; :: thesis: for x, y being set holds (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q
let x, y be set ; :: thesis: (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q
( <*y*> ^ q <> {} & (p ^ <*y*>) ^ q = p ^ (<*y*> ^ q) ) by FINSEQ_1:45;
hence (p ^ <*x*>) $^ (<*y*> ^ q) = (p ^ <*y*>) ^ q by Th2; :: thesis: verum