let f, g be FinSequence of REAL ; :: thesis: ( ( len f = len g or dom f = dom g ) implies ( len (f - g) = len f & dom (f - g) = dom f ) )
reconsider f1 = f as Element of (len f) -tuples_on REAL by FINSEQ_2:92;
assume ( len f = len g or dom f = dom g ) ; :: thesis: ( len (f - g) = len f & dom (f - g) = dom f )
then len f = len g by FINSEQ_3:29;
then reconsider g1 = g as Element of (len f) -tuples_on REAL by FINSEQ_2:92;
f1 - g1 is Element of (len f) -tuples_on REAL ;
hence len (f - g) = len f by CARD_1:def 7; :: thesis: dom (f - g) = dom f
hence dom (f - g) = dom f by FINSEQ_3:29; :: thesis: verum