defpred S₁[ set , set ] means ex x' being Element of n -tuples_on D st
( x' = $1 & $2 = F * x' );
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 x' = x as Element of n -tuples_on D ;
reconsider y = F * x' as Element of n -tuples_on D by FINSEQ_2:133;
take y ; :: thesis: S₁[x,y]
take x' ; :: thesis: ( x' = x & y = F * x' )
thus ( x' = x & y = F * x' ) ; :: 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 x' being Element of n -tuples_on D st
( x' = x & G . x = F * x' ) by A2;
hence G . p1 = F * p1 ; :: thesis: verum