let s be XFinSequence; :: thesis: for p being XFinSequence-yielding FinSequence holds
( len (s ^+ p) = len p & len (p +^ s) = len p )
let p be XFinSequence-yielding FinSequence; :: thesis: ( len (s ^+ p) = len p & len (p +^ s) = len p )
( dom (s ^+ p) = dom p & dom (p +^ s) = dom p ) by Def2, Def3;
hence ( len (s ^+ p) = len p & len (p +^ s) = len p ) by FINSEQ_3:29; :: thesis: verum