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₂ -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₁ -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

proof

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;

hence 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 ) ) by A5, A2; :: thesis: verum