defpred S₁[ object , object ] means ( $1 is FinSequence & $2 is FinSequence & ( for p, itp being FinSequence st p = $1 & itp = $2 holds
( len itp = len p & ( for i being Nat st i in dom p holds
itp . i = (F . i) . (p . i) ) ) ) );
A1: for x being object st x in doms F holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in doms F implies ex y being object st S₁[x,y] )
assume A2: x in doms F ; :: thesis: ex y being object st S₁[x,y]
reconsider P = x as FinSequence by A2;
deffunc H₁( Nat) -> set = (F . $1) . (P . $1);
consider ITP being FinSequence such that
A3: len ITP = len P and
A4: for i being Nat st i in dom ITP holds
ITP . i = H₁(i) from FINSEQ_1:sch 2();
take ITP ; :: thesis: S₁[x,ITP]
thus ( x is FinSequence & ITP is FinSequence ) by A2; :: thesis: for p, itp being FinSequence st p = x & itp = ITP holds
( len itp = len p & ( for i being Nat st i in dom p holds
itp . i = (F . i) . (p . i) ) )
let p, itp be FinSequence; :: thesis: ( p = x & itp = ITP implies ( len itp = len p & ( for i being Nat st i in dom p holds
itp . i = (F . i) . (p . i) ) ) )
assume A5: ( p = x & itp = ITP ) ; :: thesis: ( len itp = len p & ( for i being Nat st i in dom p holds
itp . i = (F . i) . (p . i) ) )
dom ITP = dom P by A3, FINSEQ_3:29;
hence ( len itp = len p & ( for i being Nat st i in dom p holds
itp . i = (F . i) . (p . i) ) ) by A5, A3, A4; :: thesis: verum

end;

consider IT being Function such that
A6: ( dom IT = doms F & ( for x being object st x in doms F holds
S₁[x,IT . x] ) ) from CLASSES1:sch 1(A1);
for x being object st x in dom IT holds
IT . x is FinSequence by A6;
then reconsider IT = IT as FinSequence-yielding Function by PRE_POLY:def 3;
take IT ; :: thesis: ( dom IT = doms F & ( for p being FinSequence st p in doms F holds
( len (IT . p) = len p & ( for i being Nat st i in dom p holds
(IT . p) . i = (F . i) . (p . i) ) ) ) )
thus ( dom IT = doms F & ( for p being FinSequence st p in doms F holds
( len (IT . p) = len p & ( for i being Nat st i in dom p holds
(IT . p) . i = (F . i) . (p . i) ) ) ) ) by A6; :: thesis: verum