let f1, f2 be sequence of (bool the carrier of T); :: thesis: ( ( for n being Nat for B being Subset of T st B = f1 . n holds f1 .(n + 1)= B ^b ) & f1 .0= A & ( for n being Nat for B being Subset of T st B = f2 . n holds f2 .(n + 1)= B ^b ) & f2 .0= A implies f1 = f2 ) assume that A2:
for n being Nat for B being Subset of T st B = f1 . n holds f1 .(n + 1)= B ^band A3:
f1 .0= A
and A4:
for n being Nat for B being Subset of T st B = f2 . n holds f2 .(n + 1)= B ^band A5:
f2 .0= A
; :: thesis: f1 = f2 defpred S1[ Nat] means f1 . $1 = f2 . $1; A6:
for n being Nat st S1[n] holds S1[n + 1]