let X be set ; :: thesis: for L being List of X

for O being Operation of X

for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))

let L be List of X; :: thesis: for O being Operation of X

for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))

let O be Operation of X; :: thesis: for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))

let n be Nat; :: thesis: L WHEREle (O,n) = L WHERElt (O,(n + 1))

thus L WHEREle (O,n) c= L WHERElt (O,(n + 1)) :: according to XBOOLE_0:def 10 :: thesis: L WHERElt (O,(n + 1)) c= L WHEREle (O,n)

assume z in L WHERElt (O,(n + 1)) ; :: thesis: z in L WHEREle (O,n)

then consider x being Element of X such that

A2: ( z = x & card (x . O) in n + 1 & x in L ) ;

Segm (n + 1) = succ (Segm n) by NAT_1:38;

then card (x . O) c= n by A2, ORDINAL1:22;

hence z in L WHEREle (O,n) by A2; :: thesis: verum

for O being Operation of X

for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))

let L be List of X; :: thesis: for O being Operation of X

for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))

let O be Operation of X; :: thesis: for n being Nat holds L WHEREle (O,n) = L WHERElt (O,(n + 1))

let n be Nat; :: thesis: L WHEREle (O,n) = L WHERElt (O,(n + 1))

thus L WHEREle (O,n) c= L WHERElt (O,(n + 1)) :: according to XBOOLE_0:def 10 :: thesis: L WHERElt (O,(n + 1)) c= L WHEREle (O,n)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHERElt (O,(n + 1)) or z in L WHEREle (O,n) )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHEREle (O,n) or z in L WHERElt (O,(n + 1)) )

assume z in L WHEREle (O,n) ; :: thesis: z in L WHERElt (O,(n + 1))

then consider x being Element of X such that

A1: ( z = x & card (x . O) c= n & x in L ) ;

Segm (n + 1) = succ (Segm n) by NAT_1:38;

then card (x . O) in n + 1 by A1, ORDINAL1:22;

hence z in L WHERElt (O,(n + 1)) by A1; :: thesis: verum

end;assume z in L WHEREle (O,n) ; :: thesis: z in L WHERElt (O,(n + 1))

then consider x being Element of X such that

A1: ( z = x & card (x . O) c= n & x in L ) ;

Segm (n + 1) = succ (Segm n) by NAT_1:38;

then card (x . O) in n + 1 by A1, ORDINAL1:22;

hence z in L WHERElt (O,(n + 1)) by A1; :: thesis: verum

assume z in L WHERElt (O,(n + 1)) ; :: thesis: z in L WHEREle (O,n)

then consider x being Element of X such that

A2: ( z = x & card (x . O) in n + 1 & x in L ) ;

Segm (n + 1) = succ (Segm n) by NAT_1:38;

then card (x . O) c= n by A2, ORDINAL1:22;

hence z in L WHEREle (O,n) by A2; :: thesis: verum