let L be non empty addLoopStr ; :: thesis: for x1, x2 being FinSequence of L st len x1 = len x2 holds
len (x1 - x2) = len x1
let x1, x2 be FinSequence of L; :: thesis: ( len x1 = len x2 implies len (x1 - x2) = len x1 )
set n = len x1;
reconsider z1 = x1 as Element of (len x1) -tuples_on the carrier of L by FINSEQ_2:92;
assume len x1 = len x2 ; :: thesis: len (x1 - x2) = len x1
then reconsider z2 = x2 as Element of (len x1) -tuples_on the carrier of L by FINSEQ_2:92;
dom (z1 - z2) = Seg (len x1) by FINSEQ_2:124;
hence len (x1 - x2) = len x1 by FINSEQ_1:def 3; :: thesis: verum