defpred S₁[ Nat, set ] means $2 = FreeOpNSG ($1,f,D);
set A = TS (DTConUA (f,D));
A1: for n being Nat st n in Seg (len f) holds
ex x being Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) st S₁[n,x]

proof

let n be Nat; :: thesis: ( n in Seg (len f) implies ex x being Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) st S₁[n,x] )
assume n in Seg (len f) ; :: thesis: ex x being Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) st S₁[n,x]
reconsider O = FreeOpNSG (n,f,D) as Element of PFuncs (((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D)))) by PARTFUN1:45;
take O ; :: thesis: S₁[n,O]
thus S₁[n,O] ; :: thesis: verum

end;

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