let f, g, h be complex-valued FinSequence; :: thesis: ( dom h = (dom f) /\ (dom g) implies len h = min ((len f),(len g)) )
assume A1: dom h = (dom f) /\ (dom g) ; :: thesis: len h = min ((len f),(len g))

per cases ( len f >= len g or len f < len g ) ;

suppose B1: len f >= len g ; :: thesis: len h = min ((len f),(len g))

then (dom f) /\ (dom g) = dom g by FINSEQ_3:30, XBOOLE_1:28;
then len h = len g by A1, FINSEQ_3:29;
hence len h = min ((len f),(len g)) by B1, XXREAL_0:def 9; :: thesis: verum

end;

suppose B1: len f < len g ; :: thesis: len h = min ((len f),(len g))

then (dom f) /\ (dom g) = dom f by FINSEQ_3:30, XBOOLE_1:28;
then len h = len f by A1, FINSEQ_3:29;
hence len h = min ((len f),(len g)) by B1, XXREAL_0:def 9; :: thesis: verum

end;

end;