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, CARD_3:def 10;
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 proj1 f = proj1 g )
assume A3: ( f in IT & g in IT ) ; :: thesis: proj1 f = proj1 g
then reconsider f = f, g = g as FinSequence ;
len f = len g by A2, A3;
hence proj1 f = proj1 g by FINSEQ_3:29; :: thesis: verum