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 ;
for k being Nat st k in dom f holds
f . k = g . k
proof
let k be Nat; :: thesis: ( k in dom f implies f . k = g . k )
defpred S1[ Nat] means ( \$1 in dom f implies f . \$1 = g . \$1 );
A17: S1[ 0 ] by FINSEQ_3:24;
A18: for a being Nat st S1[a] holds
S1[a + 1]
proof
let a be Nat; :: thesis: ( S1[a] implies S1[a + 1] )
assume that
A19: S1[a] and
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 ) ;
suppose A21: a in dom f ; :: thesis: f . (a + 1) = g . (a + 1)
then A22: f /. a = f . a by PARTFUN1:def 6
.= g /. a by ;
thus f . (a + 1) = S *' (f /. a) by
.= g . (a + 1) by A15, A16, A20, A21, A22 ; :: thesis: verum
end;
suppose not a in dom f ; :: thesis: f . (a + 1) = g . (a + 1)
then a = 0 by ;
hence f . (a + 1) = g . (a + 1) by ; :: thesis: verum
end;
end;
end;
for a being Nat holds S1[a] from hence ( k in dom f implies f . k = g . k ) ; :: thesis: verum
end;
hence S1 = S2 by ; :: thesis: verum