defpred S₁[ 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 S₁[n,x]

proof

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

end;

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
S₁[n,p . n] ) ) from FINSEQ_1:sch 5(A1);
reconsider p = p as PFuncFinSequence of (Class E) ;
take p ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum