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