let X be set ; :: thesis: for F1 being FinSequence of bool X ex A1 being SetSequence of X st

( ( for k being Nat st k in dom F1 holds

A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds

A1 . k = {} ) )

deffunc H_{1}( object ) -> set = {} ;

let F1 be FinSequence of bool X; :: thesis: ex A1 being SetSequence of X st

( ( for k being Nat st k in dom F1 holds

A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds

A1 . k = {} ) )

defpred S_{1}[ object ] means $1 in dom F1;

deffunc H_{2}( object ) -> set = F1 . $1;

ex f being Function st

( dom f = NAT & ( for k being object st k in NAT holds

( ( S_{1}[k] implies f . k = H_{2}(k) ) & ( not S_{1}[k] implies f . k = H_{1}(k) ) ) ) )
from PARTFUN1:sch 1();

then consider f being Function such that

A1: dom f = NAT and

A2: for x being object st x in NAT holds

( ( x in dom F1 implies f . x = F1 . x ) & ( not x in dom F1 implies f . x = {} ) ) ;

A3: for x being object st x in dom F1 holds

F1 . x in bool X

f . x in bool X

take f ; :: thesis: ( ( for k being Nat st k in dom F1 holds

f . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds

f . k = {} ) )

thus for k being Nat st k in dom F1 holds

f . k = F1 . k by A2; :: thesis: for k being Nat st not k in dom F1 holds

f . k = {}

let k be Nat; :: thesis: ( not k in dom F1 implies f . k = {} )

k in NAT by ORDINAL1:def 12;

hence ( not k in dom F1 implies f . k = {} ) by A2; :: thesis: verum

( ( for k being Nat st k in dom F1 holds

A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds

A1 . k = {} ) )

deffunc H

let F1 be FinSequence of bool X; :: thesis: ex A1 being SetSequence of X st

( ( for k being Nat st k in dom F1 holds

A1 . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds

A1 . k = {} ) )

defpred S

deffunc H

ex f being Function st

( dom f = NAT & ( for k being object st k in NAT holds

( ( S

then consider f being Function such that

A1: dom f = NAT and

A2: for x being object st x in NAT holds

( ( x in dom F1 implies f . x = F1 . x ) & ( not x in dom F1 implies f . x = {} ) ) ;

A3: for x being object st x in dom F1 holds

F1 . x in bool X

proof

for x being object st x in NAT holds
let x be object ; :: thesis: ( x in dom F1 implies F1 . x in bool X )

assume x in dom F1 ; :: thesis: F1 . x in bool X

then F1 . x in rng F1 by FUNCT_1:3;

hence F1 . x in bool X ; :: thesis: verum

end;assume x in dom F1 ; :: thesis: F1 . x in bool X

then F1 . x in rng F1 by FUNCT_1:3;

hence F1 . x in bool X ; :: thesis: verum

f . x in bool X

proof

then reconsider f = f as SetSequence of X by A1, FUNCT_2:3;
let x be object ; :: thesis: ( x in NAT implies f . x in bool X )

assume A4: x in NAT ; :: thesis: f . x in bool X

end;assume A4: x in NAT ; :: thesis: f . x in bool X

take f ; :: thesis: ( ( for k being Nat st k in dom F1 holds

f . k = F1 . k ) & ( for k being Nat st not k in dom F1 holds

f . k = {} ) )

thus for k being Nat st k in dom F1 holds

f . k = F1 . k by A2; :: thesis: for k being Nat st not k in dom F1 holds

f . k = {}

let k be Nat; :: thesis: ( not k in dom F1 implies f . k = {} )

k in NAT by ORDINAL1:def 12;

hence ( not k in dom F1 implies f . k = {} ) by A2; :: thesis: verum