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 H1( 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 S1[ object ] means $1 in dom F1;
deffunc H2( object ) -> set = F1 . $1;
ex f being Function st
( dom f = NAT & ( for k being object st k in NAT holds
( ( S1[k] implies f . k = H2(k) ) & ( not S1[k] implies f . k = H1(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
proof
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;
for x being object st x in NAT holds
f . x in bool X
proof
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
per cases ( not x in dom F1 or x in dom F1 ) ;
suppose A5: x in dom F1 ; :: thesis: f . x in bool X
then f . x = F1 . x by A2;
hence f . x in bool X by A3, A5; :: thesis: verum
end;
end;
end;
then reconsider f = f as SetSequence of X by A1, FUNCT_2:3;
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