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

let y be Element of F_Complex ; :: thesis: f . y = x * ((power F_Complex ) . 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)) by FUNCT_1:35
.= x * (y * y) by FUNCT_1:35
.= x * ((power F_Complex ) . y,2) by GROUP_1:99 ; :: thesis: verum

end;

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