let f, g, h be FinSequence of COMPLEX ; :: 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;