let R be non degenerated Ring; :: thesis: for X being non empty set holds IotaMap (X,R) is universal
let X be non empty set ; :: thesis: IotaMap (X,R) is universal
let N be LeftMod of R; :: according to LMODFREE:def 32 :: thesis: for v being Function of X, the carrier of N ex F being Homomorphism of id R, Free_LMod (X,R),N st
( F * (IotaMap (X,R)) = v & ( for f1, f2 being Homomorphism of id R, Free_LMod (X,R),N st f1 * (IotaMap (X,R)) = v & f2 * (IotaMap (X,R)) = v holds
f1 = f2 ) )
let v be Function of X, the carrier of N; :: thesis: ex F being Homomorphism of id R, Free_LMod (X,R),N st
( F * (IotaMap (X,R)) = v & ( for f1, f2 being Homomorphism of id R, Free_LMod (X,R),N st f1 * (IotaMap (X,R)) = v & f2 * (IotaMap (X,R)) = v holds
f1 = f2 ) )
reconsider F = Phi v as Homomorphism of id R, Free_LMod (X,R),N by Th23;
take F ; :: thesis: ( F * (IotaMap (X,R)) = v & ( for f1, f2 being Homomorphism of id R, Free_LMod (X,R),N st f1 * (IotaMap (X,R)) = v & f2 * (IotaMap (X,R)) = v holds
f1 = f2 ) )
thus F * (IotaMap (X,R)) = v by Th24; :: thesis: for f1, f2 being Homomorphism of id R, Free_LMod (X,R),N st f1 * (IotaMap (X,R)) = v & f2 * (IotaMap (X,R)) = v holds
f1 = f2
let f1, f2 be Homomorphism of id R, Free_LMod (X,R),N; :: thesis: ( f1 * (IotaMap (X,R)) = v & f2 * (IotaMap (X,R)) = v implies f1 = f2 )
assume ( f1 * (IotaMap (X,R)) = v & f2 * (IotaMap (X,R)) = v ) ; :: thesis: f1 = f2
hence f1 = f2 by Lm41; :: thesis: verum