thus ( IT is with_common_domain implies for a, b being FinSequence st a in IT & b in IT holds
len a = len b ) :: thesis: ( ( for a, b being FinSequence st a in IT & b in IT holds
len a = len b ) implies IT is with_common_domain )

proof

assume A1: IT is with_common_domain ; :: thesis: for a, b being FinSequence st a in IT & b in IT holds
len a = len b
let a, b be FinSequence; :: thesis: ( a in IT & b in IT implies len a = len b )
assume ( a in IT & b in IT ) ; :: thesis: len a = len b
then dom a = dom b by A1;
hence len a = len b by FINSEQ_3:29; :: thesis: verum

end;

assume A2: for a, b being FinSequence st a in IT & b in IT holds
len a = len b ; :: thesis: IT is with_common_domain
let f, g be Function; :: according to CARD_3:def 10 :: thesis: ( not f in IT or not g in IT or dom f = dom g )
assume A3: ( f in IT & g in IT ) ; :: thesis: dom f = dom g
then reconsider f = f, g = g as FinSequence ;
len f = len g by A2, A3;
hence dom f = dom g by FINSEQ_3:29; :: thesis: verum