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

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

$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

proof

consider p being FinSequence of PFuncs ((A *),A) such that
let n be Nat; :: thesis: ( n in Seg (len the charact of U0) implies ex x being Element of PFuncs ((A *),A) st S_{1}[n,x] )

assume n in Seg (len the charact of U0) ; :: thesis: ex x being Element of PFuncs ((A *),A) st S_{1}[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_{1}[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;assume n in Seg (len the charact of U0) ; :: thesis: ex x being Element of PFuncs ((A *),A) st S

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

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

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

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