set f = ComSign A;

defpred S_{1}[ Nat, set ] means $2 = [[:(ProdOp (A,$1)):]];

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_{1}[k,x]

A2: ( dom p = Seg (len (ComSign A)) & ( for k being Nat st k in Seg (len (ComSign A)) holds

S_{1}[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

defpred S

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

proof

consider p being FinSequence of PFuncs (((product (Carrier A)) *),(product (Carrier A))) such that
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_{1}[k,x] )

assume k in Seg (len (ComSign A)) ; :: thesis: ex x being Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) st S_{1}[k,x]

reconsider a = [[:(ProdOp (A,k)):]] as Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) by PARTFUN1:45;

take a ; :: thesis: S_{1}[k,a]

thus S_{1}[k,a]
; :: thesis: verum

end;assume k in Seg (len (ComSign A)) ; :: thesis: ex x being Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) st S

reconsider a = [[:(ProdOp (A,k)):]] as Element of PFuncs (((product (Carrier A)) *),(product (Carrier A))) by PARTFUN1:45;

take a ; :: thesis: S

thus S

A2: ( dom p = Seg (len (ComSign A)) & ( for k being Nat st k in Seg (len (ComSign A)) holds

S

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