let s be FinSequence; :: thesis: len (Op-RightShift s) = len s
A1: len <*(s . (len s))*> = 1 by FINSEQ_1:40;
len (<*(s . (len s))*> ^ s) = (len s) + 1 by A1, FINSEQ_1:22;
hence len (Op-RightShift s) = len s by FINSEQ_1:59, NAT_1:12; :: thesis: verum