let q be set ; :: thesis: for F being Group-like associative multMagma-Family of {q}

for G being Group st F = q .--> G holds

ex HFG being Homomorphism of (product F),G st

( HFG is bijective & ( for x being {q} -defined the carrier of b_{2} -valued total Function holds HFG . x = Product x ) )

let F be Group-like associative multMagma-Family of {q}; :: thesis: for G being Group st F = q .--> G holds

ex HFG being Homomorphism of (product F),G st

( HFG is bijective & ( for x being {q} -defined the carrier of b_{1} -valued total Function holds HFG . x = Product x ) )

let G be Group; :: thesis: ( F = q .--> G implies ex HFG being Homomorphism of (product F),G st

( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) ) )

assume A1: F = q .--> G ; :: thesis: ex HFG being Homomorphism of (product F),G st

( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) )

consider I being Homomorphism of G,(product F) such that

A2: ( I is bijective & ( for x being Element of G holds I . x = q .--> x ) ) by Th21, A1;

set HFG = I " ;

A3: rng I = the carrier of (product F) by A2, FUNCT_2:def 3;

then reconsider HFG = I " as Function of (product F),G by FUNCT_2:25, A2;

A4: ( HFG * I = id the carrier of G & I * HFG = id the carrier of (product F) ) by A2, A3, FUNCT_2:29;

A5: HFG is onto by A4, FUNCT_2:23;

reconsider HFG = HFG as Homomorphism of (product F),G by A2, GROUP_6:62;

for y being {q} -defined the carrier of G -valued total Function holds HFG . y = Product y

( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) ) by A5, A2; :: thesis: verum

for G being Group st F = q .--> G holds

ex HFG being Homomorphism of (product F),G st

( HFG is bijective & ( for x being {q} -defined the carrier of b

let F be Group-like associative multMagma-Family of {q}; :: thesis: for G being Group st F = q .--> G holds

ex HFG being Homomorphism of (product F),G st

( HFG is bijective & ( for x being {q} -defined the carrier of b

let G be Group; :: thesis: ( F = q .--> G implies ex HFG being Homomorphism of (product F),G st

( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) ) )

assume A1: F = q .--> G ; :: thesis: ex HFG being Homomorphism of (product F),G st

( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) )

consider I being Homomorphism of G,(product F) such that

A2: ( I is bijective & ( for x being Element of G holds I . x = q .--> x ) ) by Th21, A1;

set HFG = I " ;

A3: rng I = the carrier of (product F) by A2, FUNCT_2:def 3;

then reconsider HFG = I " as Function of (product F),G by FUNCT_2:25, A2;

A4: ( HFG * I = id the carrier of G & I * HFG = id the carrier of (product F) ) by A2, A3, FUNCT_2:29;

A5: HFG is onto by A4, FUNCT_2:23;

reconsider HFG = HFG as Homomorphism of (product F),G by A2, GROUP_6:62;

for y being {q} -defined the carrier of G -valued total Function holds HFG . y = Product y

proof

hence
ex HFG being Homomorphism of (product F),G st
let y be {q} -defined the carrier of G -valued total Function; :: thesis: HFG . y = Product y

A6: ( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) ) by A1, Th25;

reconsider z = y . q as Element of G by A1, Th25;

A7: I . z = q .--> z by A2

.= y by A1, Th25 ;

thus HFG . y = z by FUNCT_2:26, A2, A7

.= Product y by Th9, A6 ; :: thesis: verum

end;A6: ( y in the carrier of (product F) & y . q in the carrier of G & y = q .--> (y . q) ) by A1, Th25;

reconsider z = y . q as Element of G by A1, Th25;

A7: I . z = q .--> z by A2

.= y by A1, Th25 ;

thus HFG . y = z by FUNCT_2:26, A2, A7

.= Product y by Th9, A6 ; :: thesis: verum

( HFG is bijective & ( for x being {q} -defined the carrier of G -valued total Function holds HFG . x = Product x ) ) by A5, A2; :: thesis: verum