defpred S₁[ Nat, set ] means $2 = [[:(ProdOp A,$1):]];
set f = ComSign A;
A1: for k being Nat st k in Seg (len (ComSign A)) holds
ex x being Element of PFuncs ((product (Carrier A)) * ),(product (Carrier A)) st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len (ComSign A)) implies ex x being Element of PFuncs ((product (Carrier A)) * ),(product (Carrier A)) st S₁[k,x] )
assume k in Seg (len (ComSign A)) ; :: thesis: ex x being Element of PFuncs ((product (Carrier A)) * ),(product (Carrier A)) st S₁[k,x]
reconsider a = [[:(ProdOp A,k):]] as Element of PFuncs ((product (Carrier A)) * ),(product (Carrier A)) by PARTFUN1:119;
take a ; :: thesis: S₁[k,a]
thus S₁[k,a] ; :: thesis: verum

end;

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