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₁( set ) -> 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₁[ set ] means $1 in dom F1;
deffunc H₂( set ) -> set = F1 . $1;
ex f being Function st
( dom f = NAT & ( for k being set st k in NAT holds
( ( S₁[k] implies f . k = H₂(k) ) & ( not S₁[k] implies f . k = H₁(k) ) ) ) ) from PARTFUN1:sch 1();
then consider f being Function such that
A1: dom f = NAT and
A2: for x being set 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 set st x in dom F1 holds
F1 . x in bool X

proof

let x be set ; :: 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:12;
hence F1 . x in bool X ; :: thesis: verum

end;

for x being set st x in NAT holds
f . x in bool X

proof

let x be set ; :: 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 not x in dom F1 ; :: thesis: f . x in bool X

then f . x = {} by A2, A4;
then f . x c= X by XBOOLE_1:2;
hence f . x in bool X ; :: thesis: verum

end;

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:5;
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 13;
hence ( not k in dom F1 implies f . k = {} ) by A2; :: thesis: verum