let X be set ; :: thesis: for f being FinSequence of X
for g being Subset of f st len (Seq g) = len f holds
Seq g = f
let f be FinSequence of X; :: thesis: for g being Subset of f st len (Seq g) = len f holds
Seq g = f
let g be Subset of f; :: thesis: ( len (Seq g) = len f implies Seq g = f )
assume A1: len (Seq g) = len f ; :: thesis: Seq g = f
A2: len (Seq g) = card g by GLIB_001:5;

now :: thesis: not g <> f

assume g <> f ; :: thesis: contradiction
then g c< f ;
hence contradiction by A1, A2, CARD_2:48; :: thesis: verum

end;

hence Seq g = f by FINSEQ_3:116; :: thesis: verum