let R be non degenerated Ring; :: thesis: for X being non empty set
for N being LeftMod of R
for v being Function of X, the carrier of N
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 X be non empty set ; :: thesis: for N being LeftMod of R
for v being Function of X, the carrier of N
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 N be LeftMod of R; :: thesis: for v being Function of X, the carrier of N
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: 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 that
A1: f1 * (IotaMap (X,R)) = v and
A2: f2 * (IotaMap (X,R)) = v ; :: thesis: f1 = f2
for a being Element of (Free_LMod (X,R)) holds f1 . a = f2 . a

proof

let a be Element of (Free_LMod (X,R)); :: thesis: f1 . a = f2 . a
set s = F_idxseq a;
dom f1 = the carrier of (Free_LMod (X,R)) by FUNCT_2:def 1;
then A5: rng (F_idxseq a) c= dom f1 ;
dom f2 = the carrier of (Free_LMod (X,R)) by FUNCT_2:def 1;
then A6: rng (F_idxseq a) c= dom f2 ;
A7: f1 * (F_idxseq a) = f2 * (F_idxseq a)

proof

A8: dom (f1 * (F_idxseq a)) = dom (F_idxseq a) by A5, RELAT_1:27
.= dom (f2 * (F_idxseq a)) by A6, RELAT_1:27 ;
for i being object st i in dom (f1 * (F_idxseq a)) holds
(f1 * (F_idxseq a)) . i = (f2 * (F_idxseq a)) . i

proof

let i be object ; :: thesis: ( i in dom (f1 * (F_idxseq a)) implies (f1 * (F_idxseq a)) . i = (f2 * (F_idxseq a)) . i )
assume A9: i in dom (f1 * (F_idxseq a)) ; :: thesis: (f1 * (F_idxseq a)) . i = (f2 * (F_idxseq a)) . i
then reconsider k = i as Nat ;
A10: k in dom (F_idxseq a) by A9, FUNCT_1:11;
reconsider ak = (F_idxseq a) /. k as Element of (Free_LMod (X,R)) ;
A11: dom (F_idxseq a) = Seg (len (F_idxseq a)) by FINSEQ_1:def 3
.= Seg (len (idxseq a)) by Def24
.= dom (idxseq a) by FINSEQ_1:def 3 ;
then reconsider xk = (idxseq a) . k as Element of X by A9, FUNCT_1:11, FINSEQ_2:11;
A12: Support (@ ak) = {xk} by A11, A9, FUNCT_1:11, Lm24;
reconsider r = (@ ak) . xk as Element of R ;
f1 . (r * ((IotaMap (X,R)) . xk)) = ((id R) . r) * (f1 . ((IotaMap (X,R)) . xk)) by MOD_4:def 17;
then A13: f1 . ak = r * (f1 . ((IotaMap (X,R)) . xk)) by A12, Lm26;
f2 . (r * ((IotaMap (X,R)) . xk)) = ((id R) . r) * (f2 . ((IotaMap (X,R)) . xk)) by MOD_4:def 17;
then A14: f2 . ak = r * (f2 . ((IotaMap (X,R)) . xk)) by A12, Lm26;
(f1 * (F_idxseq a)) . i = f1 . ((F_idxseq a) . k) by A9, FUNCT_1:12
.= f1 . ak by A10, PARTFUN1:def 6
.= r * (v . xk) by A13, A1, FUNCT_2:15
.= f2 . ak by A14, A2, FUNCT_2:15
.= f2 . ((F_idxseq a) . k) by A10, PARTFUN1:def 6
.= (f2 * (F_idxseq a)) . i by A8, A9, FUNCT_1:12 ;
hence (f1 * (F_idxseq a)) . i = (f2 * (F_idxseq a)) . i ; :: thesis: verum

end;

hence f1 * (F_idxseq a) = f2 * (F_idxseq a) by A8; :: thesis: verum

end;

f1 . a = f1 . (Sum (F_idxseq a)) by Th15
.= Sum (f2 * (F_idxseq a)) by A7, Lm40
.= f2 . (Sum (F_idxseq a)) by Lm40
.= f2 . a by Th15 ;
hence f1 . a = f2 . a ; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum