let x be Element of F_Complex; :: thesis: ex x1 being Element of COMPLEX st
( x = x1 & FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) )
reconsider x1 = x as Element of COMPLEX by COMPLFLD:def 1;
take x1 ; :: thesis: ( x = x1 & FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) )
thus x = x1 ; :: thesis: FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX))
the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
then reconsider f = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) as Function of F_Complex,F_Complex ;

now :: thesis: for y being Element of F_Complex holds f . y = x * (power (y,2))

let y be Element of F_Complex; :: thesis: f . y = x * (power (y,2))
reconsider y1 = y as Element of COMPLEX by COMPLFLD:def 1;
thus f . y = x1 * (((id COMPLEX) (#) (id COMPLEX)) . y1) by VALUED_1:6
.= x1 * (((id COMPLEX) . y1) * ((id COMPLEX) . y1)) by VALUED_1:5
.= x1 * (y1 * ((id COMPLEX) . y1))
.= x * (y * y)
.= x * (power (y,2)) by GROUP_1:51 ; :: thesis: verum

end;

hence FPower (x,2) = x1 (#) ((id COMPLEX) (#) (id COMPLEX)) by Def12; :: thesis: verum