defpred S₁[ Nat, set ] means for o being operation of U0 st o = the charact of U0 . $1 holds
$2 = o /. A;
A1: for n being Nat st n in Seg (len the charact of U0) holds
ex x being Element of PFuncs ((A *),A) st S₁[n,x]

proof

let n be Nat; :: thesis: ( n in Seg (len the charact of U0) implies ex x being Element of PFuncs ((A *),A) st S₁[n,x] )
assume n in Seg (len the charact of U0) ; :: thesis: ex x being Element of PFuncs ((A *),A) st S₁[n,x]
then n in dom the charact of U0 by FINSEQ_1:def 3;
then reconsider o1 = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;
reconsider x = o1 /. A as Element of PFuncs ((A *),A) by PARTFUN1:45;
take x ; :: thesis: S₁[n,x]
let o be operation of U0; :: thesis: ( o = the charact of U0 . n implies x = o /. A )
assume o = the charact of U0 . n ; :: thesis: x = o /. A
hence x = o /. A ; :: thesis: verum

end;

consider p being FinSequence of PFuncs ((A *),A) such that
A2: dom p = Seg (len the charact of U0) and
A3: for n being Nat st n in Seg (len the charact of U0) holds
S₁[n,p . n] from FINSEQ_1:sch 5(A1);
reconsider p = p as PFuncFinSequence of A ;
take p ; :: thesis: ( dom p = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom p & o = the charact of U0 . n holds
p . n = o /. A ) )
thus dom p = dom the charact of U0 by A2, FINSEQ_1:def 3; :: thesis: for n being set
for o being operation of U0 st n in dom p & o = the charact of U0 . n holds
p . n = o /. A
let n be set ; :: thesis: for o being operation of U0 st n in dom p & o = the charact of U0 . n holds
p . n = o /. A
let o be operation of U0; :: thesis: ( n in dom p & o = the charact of U0 . n implies p . n = o /. A )
assume ( n in dom p & o = the charact of U0 . n ) ; :: thesis: p . n = o /. A
hence p . n = o /. A by A2, A3; :: thesis: verum