let a, b be SetSequence; :: thesis: ( ( for n being Nat holds a . n = Funcs ((X . (n + 1)),(X . n)) ) & ( for n being Nat holds b . n = Funcs ((X . (n + 1)),(X . n)) ) implies a = b )
assume that
A2: for n being Nat holds a . n = Funcs ((X . (n + 1)),(X . n)) and
A3: for n being Nat holds b . n = Funcs ((X . (n + 1)),(X . n)) ; :: thesis: a = b
let n be Element of NAT ; :: according to PBOOLE:def 21 :: thesis: a . n = b . n
a . n = Funcs ((X . (n + 1)),(X . n)) by A2;
hence a . n c= b . n by A3; :: according to XBOOLE_0:def 10 :: thesis: b . n c= a . n
a . n = Funcs ((X . (n + 1)),(X . n)) by A2;
hence b . n c= a . n by A3; :: thesis: verum