let D be non empty set ; :: thesis: for k, n being Nat
for a, b being Element of D ex g being FinSequence of D st
( len g = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )
let k, n be Nat; :: thesis: for a, b being Element of D ex g being FinSequence of D st
( len g = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )
let a, b be Element of D; :: thesis: ex g being FinSequence of D st
( len g = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies g . i = a ) & ( not i in Seg k implies g . i = b ) ) ) )
defpred S₁[ object ] means $1 in Seg k;
deffunc H₁( object ) -> Element of D = a;
deffunc H₂( object ) -> Element of D = b;
ex f being Function st
( dom f = Seg n & ( for x being object st x in Seg n holds
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(x) ) ) ) ) from PARTFUN1:sch 1();
then consider f being Function such that
A1: dom f = Seg n and
A2: for x being object st x in Seg n holds
( ( x in Seg k implies f . x = a ) & ( not x in Seg k implies f . x = b ) ) ;
reconsider p = f as FinSequence by A1, FINSEQ_1:def 2;
rng p c= D

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in D )
assume y in rng p ; :: thesis: y in D
then consider j being object such that
A3: j in dom p and
A4: y = p . j by FUNCT_1:def 3;
A5: ( not j in Seg k implies p . j = b ) by A1, A2, A3;
( j in Seg k implies p . j = a ) by A1, A2, A3;
hence y in D by A4, A5; :: thesis: verum

end;

then reconsider p = p as FinSequence of D by FINSEQ_1:def 4;
take p ; :: thesis: ( len p = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies p . i = a ) & ( not i in Seg k implies p . i = b ) ) ) )
n in NAT by ORDINAL1:def 12;
hence ( len p = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies p . i = a ) & ( not i in Seg k implies p . i = b ) ) ) ) by A1, A2, FINSEQ_1:def 3; :: thesis: verum