set A = TS (DTConUA f,D);
defpred S₁[ Nat, set ] means $2 = FreeOpZAO $1,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 = FreeOpZAO n,f,D as Element of PFuncs ((TS (DTConUA f,D)) * ),(TS (DTConUA f,D)) by PARTFUN1:119;
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 Element of NAT st n in dom p holds
p . n = FreeOpZAO n,f,D ) )
thus len p = len f by A2, FINSEQ_1:def 3; :: thesis: for n being Element of NAT st n in dom p holds
p . n = FreeOpZAO n,f,D
let n be Element of NAT ; :: thesis: ( n in dom p implies p . n = FreeOpZAO n,f,D )
assume n in dom p ; :: thesis: p . n = FreeOpZAO n,f,D
hence p . n = FreeOpZAO n,f,D by A2; :: thesis: verum