let a, b be SetSequence; :: thesis: ( ( for n being Nat holds a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ) & ( for n being Nat holds b . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ) implies a = b )

assume that

A2: for n being Nat holds a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } and

A3: for n being Nat holds b . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ; :: thesis: a = b

let n be Element of NAT ; :: according to PBOOLE:def 21 :: thesis: a . n = b . n

a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A2;

hence a . n c= b . n by A3; :: according to XBOOLE_0:def 10 :: thesis: b . n c= a . n

a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A2;

hence b . n c= a . n by A3; :: thesis: verum

assume that

A2: for n being Nat holds a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } and

A3: for n being Nat holds b . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } ; :: thesis: a = b

let n be Element of NAT ; :: according to PBOOLE:def 21 :: thesis: a . n = b . n

a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A2;

hence a . n c= b . n by A3; :: according to XBOOLE_0:def 10 :: thesis: b . n c= a . n

a . n = { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A2;

hence b . n c= a . n by A3; :: thesis: verum