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 A2: ( ( 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 } ) ) ; :: thesis: a = b

now

let n be set ; :: thesis: ( n in NAT implies a . n c= b . n )
assume n in NAT ; :: thesis: a . n c= b . n
then reconsider n1 = n as Element of NAT ;
( a . n1 = { f where f is Element of Funcs (Seg n1),(Seg (n1 + 1)) : @ f is increasing } & b . n1 = { f where f is Element of Funcs (Seg n1),(Seg (n1 + 1)) : @ f is increasing } ) by A2;
hence a . n c= b . n ; :: thesis: verum

end;

then A3: a c= b by PBOOLE:def 5;

now

let n be set ; :: thesis: ( n in NAT implies b . n c= a . n )
assume n in NAT ; :: thesis: b . n c= a . n
then reconsider n1 = n as Element of NAT ;
( a . n1 = { f where f is Element of Funcs (Seg n1),(Seg (n1 + 1)) : @ f is increasing } & b . n1 = { f where f is Element of Funcs (Seg n1),(Seg (n1 + 1)) : @ f is increasing } ) by A2;
hence b . n c= a . n ; :: thesis: verum

end;

then b c= a by PBOOLE:def 5;
hence a = b by A3, PBOOLE:def 13; :: thesis: verum