let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for p, q being FinSequence of FreeAtoms H st ( for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")] ) holds
for k being Nat
for i being Element of I
for g, h being Element of (H . i) st p . k = [i,g] & g * h = 1_ (H . i) holds
(Rev q) . k = [i,h]
let H be Group-like associative multMagma-Family of I; :: thesis: for p, q being FinSequence of FreeAtoms H st ( for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")] ) holds
for k being Nat
for i being Element of I
for g, h being Element of (H . i) st p . k = [i,g] & g * h = 1_ (H . i) holds
(Rev q) . k = [i,h]
let p, q be FinSequence of FreeAtoms H; :: thesis: ( ( for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")] ) implies for k being Nat
for i being Element of I
for g, h being Element of (H . i) st p . k = [i,g] & g * h = 1_ (H . i) holds
(Rev q) . k = [i,h] )
assume A1: for k being Nat
for i being Element of I
for g being Element of (H . i) st p . k = [i,g] holds
(Rev q) . k = [i,(g ")] ; :: thesis: for k being Nat
for i being Element of I
for g, h being Element of (H . i) st p . k = [i,g] & g * h = 1_ (H . i) holds
(Rev q) . k = [i,h]
let k be Nat; :: thesis: for i being Element of I
for g, h being Element of (H . i) st p . k = [i,g] & g * h = 1_ (H . i) holds
(Rev q) . k = [i,h]
let i be Element of I; :: thesis: for g, h being Element of (H . i) st p . k = [i,g] & g * h = 1_ (H . i) holds
(Rev q) . k = [i,h]
let g, h be Element of (H . i); :: thesis: ( p . k = [i,g] & g * h = 1_ (H . i) implies (Rev q) . k = [i,h] )
assume A2: ( p . k = [i,g] & g * h = 1_ (H . i) ) ; :: thesis: (Rev q) . k = [i,h]
then h = g " by GROUP_1:12;
hence (Rev q) . k = [i,h] by A1, A2; :: thesis: verum