let n be Nat; :: thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A
let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A
let A1 be SetSequence of X; :: thesis: (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A
reconsider X1 = superior_setsequence A1 as SetSequence of X ;
reconsider X2 = superior_setsequence (A1 (\) A) as SetSequence of X ;
A1: (X1 . n) \ A c= X2 . n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X1 . n) \ A or x in X2 . n )
assume A2: x in (X1 . n) \ A ; :: thesis: x in X2 . n
then A3: not x in A by XBOOLE_0:def 5;
A4: x in X1 . n by A2, XBOOLE_0:def 5;
ex k being Nat st x in (A1 (\) A) . (n + k)

proof

consider k being Nat such that
A5: x in A1 . (n + k) by A4, SETLIM_1:20;
x in (A1 . (n + k)) \ A by A3, A5, XBOOLE_0:def 5;
then x in (A1 (\) A) . (n + k) by Def8;
hence ex k being Nat st x in (A1 (\) A) . (n + k) ; :: thesis: verum

end;

hence x in X2 . n by SETLIM_1:20; :: thesis: verum

end;

X2 . n c= (X1 . n) \ A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X2 . n or x in (X1 . n) \ A )
assume A6: x in X2 . n ; :: thesis: x in (X1 . n) \ A
A7: ex k being Nat st
( x in A1 . (n + k) & not x in A )

proof

consider k being Nat such that
A8: x in (A1 (\) A) . (n + k) by A6, SETLIM_1:20;
x in (A1 . (n + k)) \ A by A8, Def8;
then ( x in A1 . (n + k) & not x in A ) by XBOOLE_0:def 5;
hence ex k being Nat st
( x in A1 . (n + k) & not x in A ) ; :: thesis: verum

end;

then x in X1 . n by SETLIM_1:20;
hence x in (X1 . n) \ A by A7, XBOOLE_0:def 5; :: thesis: verum

end;

hence (superior_setsequence (A1 (\) A)) . n = ((superior_setsequence A1) . n) \ A by A1; :: thesis: verum