let X be non empty set ; :: thesis: for fs being FinSequence of X
for fss being Subset of fs holds Seq fss,fss are_fiberwise_equipotent
let fs be FinSequence of X; :: thesis: for fss being Subset of fs holds Seq fss,fss are_fiberwise_equipotent
let fss be Subset of fs; :: thesis: Seq fss,fss are_fiberwise_equipotent
dom fss c= dom fs by RELAT_1:11;
then A0: dom fss c= Seg (len fs) by FINSEQ_1:def 3;
then A1: fss is FinSubsequence by FINSEQ_1:def 12;
then A2: Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 14;
A3: rng (Sgm (dom fss)) = dom fss by A1, FINSEQ_1:50;
then A4: dom (Sgm (dom fss)) = dom (Seq fss) by A2, RELAT_1:27;
now :: thesis: for x1, x2 being object st x1 in dom (Sgm (dom fss)) & x2 in dom (Sgm (dom fss)) & (Sgm (dom fss)) . x1 = (Sgm (dom fss)) . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom (Sgm (dom fss)) & x2 in dom (Sgm (dom fss)) & (Sgm (dom fss)) . x1 = (Sgm (dom fss)) . x2 implies x1 = x2 )
assume A5: ( x1 in dom (Sgm (dom fss)) & x2 in dom (Sgm (dom fss)) & (Sgm (dom fss)) . x1 = (Sgm (dom fss)) . x2 ) ; :: thesis: x1 = x2
reconsider i1 = x1, i2 = x2 as Nat by A5;
reconsider k1 = (Sgm (dom fss)) . i1, k2 = (Sgm (dom fss)) . i2 as Nat ;
A6: ( 1 <= i1 & 1 <= i2 & i1 <= len (Sgm (dom fss)) & i2 <= len (Sgm (dom fss)) ) by A5, FINSEQ_3:25;
now :: thesis: not i1 <> i2
assume i1 <> i2 ; :: thesis: contradiction
then ( i1 < i2 or i1 > i2 ) by XXREAL_0:1;
hence contradiction by A5, A0, A6, FINSEQ_1:def 13; :: thesis: verum
end;
hence x1 = x2 ; :: thesis: verum
end;
hence Seq fss,fss are_fiberwise_equipotent by A2, A3, A4, CLASSES1:77, FUNCT_1:def 4; :: thesis: verum