defpred S₁[ object , object ] means ( ( not $1 in X implies $2 = f . $1 ) & ( $1 in X implies $2 = (the_inverseOp_wrt B) . (f . $1) ) );
A1: for k being Nat st k in Seg (len f) holds
ex x being Element of D st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len f) implies ex x being Element of D st S₁[k,x] )
assume A2: k in Seg (len f) ; :: thesis: ex x being Element of D st S₁[k,x]
k in dom f by A2, FINSEQ_1:def 3;
then A3: ( f . k in rng f & rng f c= D ) by FUNCT_1:def 3;
then reconsider fk = f . k as Element of D ;
A4: (the_inverseOp_wrt B) . fk is Element of D ;

per cases ( k in X or not k in X ) ;

suppose k in X ; :: thesis: ex x being Element of D st S₁[k,x]

hence ex x being Element of D st S₁[k,x] by A4; :: thesis: verum

end;

suppose not k in X ; :: thesis: ex x being Element of D st S₁[k,x]

hence ex x being Element of D st S₁[k,x] by A3; :: thesis: verum

end;

end;

end;

consider p being FinSequence of D such that
A5: ( dom p = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 5(A1);
take p ; :: thesis: ( dom p = dom f & ( for i being Nat st i in dom p holds
( ( i in X implies p . i = (the_inverseOp_wrt B) . (f . i) ) & ( not i in X implies p . i = f . i ) ) ) )
thus ( dom p = dom f & ( for i being Nat st i in dom p holds
( ( i in X implies p . i = (the_inverseOp_wrt B) . (f . i) ) & ( not i in X implies p . i = f . i ) ) ) ) by A5, FINSEQ_1:def 3; :: thesis: verum