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

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 );
A17: S₁[ 0 ] by FINSEQ_3:24;
A18: 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
A19: S₁[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 A16, A19, A21, PARTFUN1:def 6 ;
thus f . (a + 1) = S *' (f /. a) by A11, A20, A21
.= 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 A20, TOPREALA:2;
hence f . (a + 1) = g . (a + 1) by A10, A14; :: thesis: verum

end;

end;

end;

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

end;

hence S1 = S2 by A8, A12, A9, A13, A16, FINSEQ_1:13; :: thesis: verum