let V, A be set ; :: thesis: for S1, S2 being FinSequence st S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 +* S2 = S1 holds
S1 +* S2 = S2
let S1, S2 be FinSequence; :: thesis: ( S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A & not S1 +* S2 = S1 implies S1 +* S2 = S2 )
assume ( S1 IsNDRankSeq V,A & S2 IsNDRankSeq V,A ) ; :: thesis: ( S1 +* S2 = S1 or S1 +* S2 = S2 )
then A1: S1 +* S2 = S2 +* S1 by Th21, FUNCT_4:34;
( dom S1 c= dom S2 or dom S2 c= dom S1 ) by Th3;
hence ( S1 +* S2 = S1 or S1 +* S2 = S2 ) by A1, FUNCT_4:19; :: thesis: verum