let S1, S2 be Subset of K; :: thesis: ( ( n = 0 & S1 = the carrier of K & S2 = the carrier of K implies S1 = S2 ) & ( not n = 0 & ex f being FinSequence of bool the carrier of K st

( S1 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) & ex f being FinSequence of bool the carrier of K st

( S2 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) implies S1 = S2 ) )

thus ( n = 0 & S1 = the carrier of K & S2 = the carrier of K implies S1 = S2 ) ; :: thesis: ( not n = 0 & ex f being FinSequence of bool the carrier of K st

( S1 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) & ex f being FinSequence of bool the carrier of K st

( S2 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) implies S1 = S2 )

assume n <> 0 ; :: thesis: ( for f being FinSequence of bool the carrier of K holds

( not S1 = f . (len f) or not len f = n or not f . 1 = S or ex i being Nat st

( i in dom f & i + 1 in dom f & not f . (i + 1) = S *' (f /. i) ) ) or for f being FinSequence of bool the carrier of K holds

( not S2 = f . (len f) or not len f = n or not f . 1 = S or ex i being Nat st

( i in dom f & i + 1 in dom f & not f . (i + 1) = S *' (f /. i) ) ) or S1 = S2 )

given f being FinSequence of bool the carrier of K such that A8: S1 = f . (len f) and

A9: len f = n and

A10: f . 1 = S and

A11: for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ; :: thesis: ( for f being FinSequence of bool the carrier of K holds

( not S2 = f . (len f) or not len f = n or not f . 1 = S or ex i being Nat st

( i in dom f & i + 1 in dom f & not f . (i + 1) = S *' (f /. i) ) ) or S1 = S2 )

given g being FinSequence of bool the carrier of K such that A12: S2 = g . (len g) and

A13: len g = n and

A14: g . 1 = S and

A15: for i being Nat st i in dom g & i + 1 in dom g holds

g . (i + 1) = S *' (g /. i) ; :: thesis: S1 = S2

A16: dom f = dom g by A9, A13, FINSEQ_3:29;

for k being Nat st k in dom f holds

f . k = g . k

( S1 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) & ex f being FinSequence of bool the carrier of K st

( S2 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) implies S1 = S2 ) )

thus ( n = 0 & S1 = the carrier of K & S2 = the carrier of K implies S1 = S2 ) ; :: thesis: ( not n = 0 & ex f being FinSequence of bool the carrier of K st

( S1 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) & ex f being FinSequence of bool the carrier of K st

( S2 = f . (len f) & len f = n & f . 1 = S & ( for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ) ) implies S1 = S2 )

assume n <> 0 ; :: thesis: ( for f being FinSequence of bool the carrier of K holds

( not S1 = f . (len f) or not len f = n or not f . 1 = S or ex i being Nat st

( i in dom f & i + 1 in dom f & not f . (i + 1) = S *' (f /. i) ) ) or for f being FinSequence of bool the carrier of K holds

( not S2 = f . (len f) or not len f = n or not f . 1 = S or ex i being Nat st

( i in dom f & i + 1 in dom f & not f . (i + 1) = S *' (f /. i) ) ) or S1 = S2 )

given f being FinSequence of bool the carrier of K such that A8: S1 = f . (len f) and

A9: len f = n and

A10: f . 1 = S and

A11: for i being Nat st i in dom f & i + 1 in dom f holds

f . (i + 1) = S *' (f /. i) ; :: thesis: ( for f being FinSequence of bool the carrier of K holds

( not S2 = f . (len f) or not len f = n or not f . 1 = S or ex i being Nat st

( i in dom f & i + 1 in dom f & not f . (i + 1) = S *' (f /. i) ) ) or S1 = S2 )

given g being FinSequence of bool the carrier of K such that A12: S2 = g . (len g) and

A13: len g = n and

A14: g . 1 = S and

A15: for i being Nat st i in dom g & i + 1 in dom g holds

g . (i + 1) = S *' (g /. i) ; :: thesis: S1 = S2

A16: dom f = dom g by A9, A13, FINSEQ_3:29;

for k being Nat st k in dom f holds

f . k = g . k

proof

hence
S1 = S2
by A8, A12, A9, A13, A16, FINSEQ_1:13; :: thesis: verum
let k be Nat; :: thesis: ( k in dom f implies f . k = g . k )

defpred S_{1}[ Nat] means ( $1 in dom f implies f . $1 = g . $1 );

A17: S_{1}[ 0 ]
by FINSEQ_3:24;

A18: for a being Nat st S_{1}[a] holds

S_{1}[a + 1]
_{1}[a]
from NAT_1:sch 2(A17, A18);

hence ( k in dom f implies f . k = g . k ) ; :: thesis: verum

end;defpred S

A17: S

A18: for a being Nat st S

S

proof

for a being Nat holds S
let a be Nat; :: thesis: ( S_{1}[a] implies S_{1}[a + 1] )

assume that

A19: S_{1}[a]
and

A20: a + 1 in dom f ; :: thesis: f . (a + 1) = g . (a + 1)

end;assume that

A19: S

A20: a + 1 in dom f ; :: thesis: f . (a + 1) = g . (a + 1)

per cases
( a in dom f or not a in dom f )
;

end;

hence ( k in dom f implies f . k = g . k ) ; :: thesis: verum