let x be object ; :: thesis: for p, q being FinSequence holds ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x
let p, q be FinSequence; :: thesis: ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x
set s = p ^ q;
((p ^ q) ^ <*x*>) . ((len (p ^ q)) + 1) = x by FINSEQ_1:42;
hence ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x by FINSEQ_1:22; :: thesis: verum