defpred S₁[ set , set ] means for m being Nat st m = f . $1 holds
$2 = TrivialOp m;
A1: for k being Nat st k in Seg (len f) holds
ex x being Element of PFuncs (({{}} *),{{}}) st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len f) implies ex x being Element of PFuncs (({{}} *),{{}}) st S₁[k,x] )
assume k in Seg (len f) ; :: thesis: ex x being Element of PFuncs (({{}} *),{{}}) st S₁[k,x]
then k in dom f by FINSEQ_1:def 3;
then reconsider k1 = f . k as Element of NAT by FINSEQ_2:11;
reconsider A = TrivialOp k1 as Element of PFuncs (({{}} *),{{}}) by PARTFUN1:45;
take A ; :: thesis: S₁[k,A]
let m be Nat; :: thesis: ( m = f . k implies A = TrivialOp m )
assume m = f . k ; :: thesis: A = TrivialOp m
hence A = TrivialOp m ; :: thesis: verum

end;

consider p being FinSequence of PFuncs (({{}} *),{{}}) such that
A2: ( dom p = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 5(A1);
reconsider p = p as PFuncFinSequence of {{}} ;
take p ; :: thesis: ( len p = len f & ( for n being Nat st n in dom p holds
for m being Nat st m = f . n holds
p . n = TrivialOp m ) )
thus len p = len f by A2, FINSEQ_1:def 3; :: thesis: for n being Nat st n in dom p holds
for m being Nat st m = f . n holds
p . n = TrivialOp m
let n be Nat; :: thesis: ( n in dom p implies for m being Nat st m = f . n holds
p . n = TrivialOp m )
assume n in dom p ; :: thesis: for m being Nat st m = f . n holds
p . n = TrivialOp m
hence for m being Nat st m = f . n holds
p . n = TrivialOp m by A2; :: thesis: verum