defpred S1[ set , set ] means for o being Element of Operations U1 st o = the charact of U1 . $1 holds
$2 = QuotOp (o,E);
A1:
for n being Nat st n in Seg (len the charact of U1) holds
ex x being Element of PFuncs (((Class E) *),(Class E)) st S1[n,x]
consider p being FinSequence of PFuncs (((Class E) *),(Class E)) such that
A2:
( dom p = Seg (len the charact of U1) & ( for n being Nat st n in Seg (len the charact of U1) holds
S1[n,p . n] ) )
from FINSEQ_1:sch 5(A1);
reconsider p = p as PFuncFinSequence of (Class E) ;
take
p
; ( len p = len the charact of U1 & ( for n being Nat st n in dom p holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
p . n = QuotOp (o1,E) ) )
thus
len p = len the charact of U1
by A2, FINSEQ_1:def 3; for n being Nat st n in dom p holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
p . n = QuotOp (o1,E)
let n be Nat; ( n in dom p implies for o1 being operation of U1 st the charact of U1 . n = o1 holds
p . n = QuotOp (o1,E) )
assume
n in dom p
; for o1 being operation of U1 st the charact of U1 . n = o1 holds
p . n = QuotOp (o1,E)
hence
for o1 being operation of U1 st the charact of U1 . n = o1 holds
p . n = QuotOp (o1,E)
by A2; verum