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 A10: S1 = f . (len f) and
A11: len f = n and
A12: f . 1 = S and
A13: 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 A14: S2 = g . (len g) and
A15: len g = n and
A16: g . 1 = S and
A17: for i being Nat st i in dom g & i + 1 in dom g holds
g . (i + 1) = S *' (g /. i) ; :: thesis: S1 = S2
A18: dom f = dom g by A11, A15, FINSEQ_3:29;
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 S₁[ Nat] means ( $1 in dom f implies f . $1 = g . $1 );
A19: S₁[ 0 ] by FINSEQ_3:24;
A20: for a being Nat st S₁[a] holds
S₁[a + 1]

proof

let a be Nat; :: thesis: ( S₁[a] implies S₁[a + 1] )
assume that
A21: S₁[a] and
A22: 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 A23: a in dom f ; :: thesis: f . (a + 1) = g . (a + 1)

then A24: f /. a = f . a by PARTFUN1:def 6
.= g /. a by A18, A21, A23, PARTFUN1:def 6 ;
thus f . (a + 1) = S *' (f /. a) by A13, A22, A23
.= g . (a + 1) by A17, A18, A22, A23, A24 ; :: thesis: verum

end;

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

then a = 0 by A22, TOPREALA:2;
hence f . (a + 1) = g . (a + 1) by A12, A16; :: thesis: verum

end;

end;

end;

for a being Nat holds S₁[a] from NAT_1:sch 2(A19, A20);
hence ( k in dom f implies f . k = g . k ) ; :: thesis: verum

end;

hence S1 = S2 by A10, A14, A11, A15, A18, FINSEQ_1:13; :: thesis: verum