let q be set ; 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 b2 -valued total Function holds HFG . x = Product x ) )
let F be 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 b1 -valued total Function holds HFG . x = Product x ) )
let G be Group; ( 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
; 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
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; verum