defpred S_{1}[ 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_{1}[x,y]

A2: for x being Element of n -tuples_on D holds S_{1}[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

( 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

proof

consider G being UnOp of (n -tuples_on D) such that
let x be Element of n -tuples_on D; :: thesis: ex y being Element of n -tuples_on D st S_{1}[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_{1}[x,y]

take x9 ; :: thesis: ( x9 = x & y = F * x9 )

thus ( x9 = x & y = F * x9 ) ; :: thesis: verum

end;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

take x9 ; :: thesis: ( x9 = x & y = F * x9 )

thus ( x9 = x & y = F * x9 ) ; :: thesis: verum

A2: for x being Element of n -tuples_on D holds S

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