defpred S1[ 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 S1[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 S1[n,x] )
assume n in Seg (len the charact of U0) ; :: thesis: ex x being Element of PFuncs ((A *),A) st S1[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: S1[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
S1[n,p . n] from 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 ; :: 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