let A be Ring; :: thesis: for X being non empty set
for f being Function of A,X
for a, b being Element of X st f is bijective holds
f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X
let X be non empty set ; :: thesis: for f being Function of A,X
for a, b being Element of X st f is bijective holds
f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X
let f be Function of A,X; :: thesis: for a, b being Element of X st f is bijective holds
f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X
let a, b be Element of X; :: thesis: ( f is bijective implies f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X )
assume A1: f is bijective ; :: thesis: f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X
then A2: rng f = X by FUNCT_2:def 3;
A3: dom f = [#] A by FUNCT_2:def 1;
reconsider x = (f ") . a, y = (f ") . b as Element of [#] A by A3, A2, A1, FUNCT_1:32;
reconsider z = the addF of A . (x,y) as Element of [#] A ;
f . z in X ;
hence f . ( the addF of A . (((f ") . a),((f ") . b))) is Element of X ; :: thesis: verum