consider f being Function such that
A1: ( A . s = f & dom f = E & rng f c= E ) by FUNCT_2:def 2;
reconsider f = f as Function of E,E by A1, FUNCT_2:4;

now

take f = f; :: thesis: f = A . s
thus f = A . s by A1; :: thesis: verum

end;

hence ^ is Function of E,E ; :: thesis: verum