set f = ComSign A;
defpred S1[ Nat, set ] means \$2 = [[:(ProdOp (A,\$1)):]];
A1: for k being Nat st k in Seg (len ()) holds
ex x being Element of PFuncs (((product ()) *),(product ())) st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len ()) implies ex x being Element of PFuncs (((product ()) *),(product ())) st S1[k,x] )
assume k in Seg (len ()) ; :: thesis: ex x being Element of PFuncs (((product ()) *),(product ())) st S1[k,x]
reconsider a = [[:(ProdOp (A,k)):]] as Element of PFuncs (((product ()) *),(product ())) by PARTFUN1:45;
take a ; :: thesis: S1[k,a]
thus S1[k,a] ; :: thesis: verum
end;
consider p being FinSequence of PFuncs (((product ()) *),(product ())) such that
A2: ( dom p = Seg (len ()) & ( for k being Nat st k in Seg (len ()) holds
S1[k,p . k] ) ) from reconsider p = p as PFuncFinSequence of (product ()) ;
take p ; :: thesis: ( len p = len () & ( for n being Nat st n in dom p holds
p . n = [[:(ProdOp (A,n)):]] ) )

thus len p = len () by ; :: 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