defpred S₁[ set , set ] means ex x9 being Element of n -tuples_on D st
( x9 = $1 & $2 = F * x9 );
A1: for x being Element of n -tuples_on D ex y being Element of n -tuples_on D st S₁[x,y]

proof

let x be Element of n -tuples_on D; :: thesis: ex y being Element of n -tuples_on D st S₁[x,y]
reconsider x9 = x as Element of n -tuples_on D ;
reconsider y = F * x9 as Element of n -tuples_on D by FINSEQ_2:113;
take y ; :: thesis: S₁[x,y]
take x9 ; :: thesis: ( x9 = x & y = F * x9 )
thus ( x9 = x & y = F * x9 ) ; :: thesis: verum

end;

consider G being UnOp of (n -tuples_on D) such that
A2: for x being Element of n -tuples_on D holds S₁[x,G . x] from FUNCT_2:sch 3(A1);
take G ; :: thesis: for x being Element of n -tuples_on D holds G . x = F * x
let p1 be Element of n -tuples_on D; :: thesis: G . p1 = F * p1
reconsider x = p1 as Element of n -tuples_on D ;
ex x9 being Element of n -tuples_on D st
( x9 = x & G . x = F * x9 ) by A2;
hence G . p1 = F * p1 ; :: thesis: verum