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