let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( not x in dom <:F:> or not y in dom <:F:> or len x = len y )
assume A1: ( x in dom <:F:> & y in dom <:F:> ) ; :: thesis: len x = len y
dom <:F:> c= (arity F) -tuples_on X by Th45;
then ( len x = arity F & len y = arity F ) by A1, FINSEQ_1:def 18;
hence len x = len y ; :: thesis: verum