let k, n be Nat; :: thesis: for D being set
for e1, e2 being FinSequence of D ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) )
let D be set ; :: thesis: for e1, e2 being FinSequence of D ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) )
let e1, e2 be FinSequence of D; :: thesis: ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) )
( e1 in D * & e2 in D * ) by FINSEQ_1:def 11;
hence ex e being FinSequence of D * st
( len e = n & ( for i being Nat st i in Seg n holds
( ( i in Seg k implies e . i = e1 ) & ( not i in Seg k implies e . i = e2 ) ) ) ) by Th2; :: thesis: verum