let S be non empty finite set ; :: thesis: for X being Subset of S
for s, t being FinSequence of S
for SD being Subset of (dom s)
for x being Subset of X st SD = s " X & t = extract (s,SD) holds
card (s " x) = card (t " x)
let X be Subset of S; :: thesis: for s, t being FinSequence of S
for SD being Subset of (dom s)
for x being Subset of X st SD = s " X & t = extract (s,SD) holds
card (s " x) = card (t " x)
let s, t be FinSequence of S; :: thesis: for SD being Subset of (dom s)
for x being Subset of X st SD = s " X & t = extract (s,SD) holds
card (s " x) = card (t " x)
let SD be Subset of (dom s); :: thesis: for x being Subset of X st SD = s " X & t = extract (s,SD) holds
card (s " x) = card (t " x)
let x be Subset of X; :: thesis: ( SD = s " X & t = extract (s,SD) implies card (s " x) = card (t " x) )
assume A1: ( SD = s " X & t = extract (s,SD) ) ; :: thesis: card (s " x) = card (t " x)
reconsider SD = SD as finite set ;
set f = (canFS SD) " ;
len t = card SD by A1, Th11;
then A2: dom t = Seg (card SD) by FINSEQ_1:def 3;
then reconsider g = (canFS SD) " as Function of SD,(dom t) by FINSEQ_1:95;
A3: (canFS SD) .: (t " x) = ((canFS SD) ") " (t " x) by FUNCT_1:84
.= (t * ((canFS SD) ")) " x by RELAT_1:146
.= (s | SD) " x by A1, Th12
.= SD /\ (s " x) by FUNCT_1:70
.= s " x by A1, RELAT_1:143, XBOOLE_1:28 ;
then A4: card (s " x) c= card (t " x) by CARD_1:66;
A5: t " x c= Seg (card SD) by A2, RELAT_1:132;
len (canFS SD) = card SD by FINSEQ_1:93;
then A6: t " x is Subset of (dom (canFS SD)) by A5, FINSEQ_1:def 3;
A7: ((canFS SD) ") * (canFS SD) = id (dom (canFS SD)) by FUNCT_1:39;
((canFS SD) ") .: (s " x) = (((canFS SD) ") * (canFS SD)) .: (t " x) by A3, RELAT_1:126
.= t " x by A6, A7, FUNCT_1:92 ;
then card (t " x) c= card (s " x) by CARD_1:66;
hence card (s " x) = card (t " x) by A4, XBOOLE_0:def 10; :: thesis: verum