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;

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

hence
Seq g = f
by FINSEQ_3:116; :: thesis: verumassume
g <> f
; :: thesis: contradiction

then g c< f ;

hence contradiction by A1, A2, CARD_2:48; :: thesis: verum

end;then g c< f ;

hence contradiction by A1, A2, CARD_2:48; :: thesis: verum