let x, y be object ; :: thesis: for F being finite set
for E being Enumeration of F st not y in union F holds
Ext (E,x,y) is Enumeration of Ext (F,x,y)
let F be finite set ; :: thesis: for E being Enumeration of F st not y in union F holds
Ext (E,x,y) is Enumeration of Ext (F,x,y)
let E be Enumeration of F; :: thesis: ( not y in union F implies Ext (E,x,y) is Enumeration of Ext (F,x,y) )
assume A1: not y in union F ; :: thesis: Ext (E,x,y) is Enumeration of Ext (F,x,y)
set S = Ext (E,x,y);
A2: ( dom (Ext (E,x,y)) = dom E & dom E = Seg (len E) ) by Def5, FINSEQ_1:def 3;
A3: rng E = F by RLAFFIN3:def 1;
A4: rng (Ext (E,x,y)) c= Ext (F,x,y)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng (Ext (E,x,y)) or a in Ext (F,x,y) )
assume a in rng (Ext (E,x,y)) ; :: thesis: a in Ext (F,x,y)
then consider c being object such that
A5: ( c in dom (Ext (E,x,y)) & (Ext (E,x,y)) . c = a ) by FUNCT_1:def 3;
A6: E . c in rng E by A5, A2, FUNCT_1:def 3;

per cases ( x in E . c or not x in E . c ) ;

suppose A7: x in E . c ; :: thesis: a in Ext (F,x,y)

then (Ext (E,x,y)) . c = (E . c) \/ {y} by A5, A2, Def5;
then (Ext (E,x,y)) . c in { (A \/ {y}) where A is Element of F : x in A } by A7, A6;
hence a in Ext (F,x,y) by A5, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A8: not x in E . c ; :: thesis: a in Ext (F,x,y)

then (Ext (E,x,y)) . c = E . c by A5, A2, Def5;
then (Ext (E,x,y)) . c in { A where A is Element of F : ( not x in A & A in F ) } by A8, A6;
hence a in Ext (F,x,y) by A5, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

Ext (F,x,y) c= rng (Ext (E,x,y))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Ext (F,x,y) or a in rng (Ext (E,x,y)) )
assume a in Ext (F,x,y) ; :: thesis: a in rng (Ext (E,x,y))

per cases then ( a in { (A \/ {y}) where A is Element of F : x in A } or a in { A where A is Element of F : ( not x in A & A in F ) } ) by XBOOLE_0:def 3;

suppose a in { (A \/ {y}) where A is Element of F : x in A } ; :: thesis: a in rng (Ext (E,x,y))

then consider A being Element of F such that
A9: ( a = A \/ {y} & x in A ) ;
F <> {} by A9, SUBSET_1:def 1;
then consider b being object such that
A10: ( b in dom E & E . b = A ) by A3, FUNCT_1:def 3;
(Ext (E,x,y)) . b = (E . b) \/ {y} by Def5, A9, A10;
hence a in rng (Ext (E,x,y)) by A9, A10, A2, FUNCT_1:def 3; :: thesis: verum

end;

suppose a in { A where A is Element of F : ( not x in A & A in F ) } ; :: thesis: a in rng (Ext (E,x,y))

then consider A being Element of F such that
A11: ( a = A & not x in A & A in F ) ;
consider b being object such that
A12: ( b in dom E & E . b = A ) by A11, A3, FUNCT_1:def 3;
(Ext (E,x,y)) . b = E . b by Def5, A11, A12;
hence a in rng (Ext (E,x,y)) by A11, A12, A2, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

then A13: Ext (F,x,y) = rng (Ext (E,x,y)) by A4;
A14: card (Ext (F,x,y)) = card F by A1, Th10;
( card F = len E & len E = len (Ext (E,x,y)) ) by CARD_1:def 7;
then Ext (E,x,y) is one-to-one by A13, A14, FINSEQ_4:62;
hence Ext (E,x,y) is Enumeration of Ext (F,x,y) by A13, RLAFFIN3:def 1; :: thesis: verum