let Q, Q2 be multLoop; :: thesis: for f being homomorphic Function of Q,Q2
for h being Function of Q,Q st h in Mlt (Ker f) holds
f * h = f
let f be homomorphic Function of Q,Q2; :: thesis: for h being Function of Q,Q st h in Mlt (Ker f) holds
f * h = f
set H = Ker f;
defpred S3[ Function of Q,Q] means f * $1 = f;
A1: for u being Element of Q st u in Ker f holds
for h being Function of Q,Q st ( for x being Element of Q holds h . x = x * u ) holds
S3[h]
proof
let u be Element of Q; :: thesis: ( u in Ker f implies for h being Function of Q,Q st ( for x being Element of Q holds h . x = x * u ) holds
S3[h] )
assume A2: u in Ker f ; :: thesis: for h being Function of Q,Q st ( for x being Element of Q holds h . x = x * u ) holds
S3[h]
let h be Function of Q,Q; :: thesis: ( ( for x being Element of Q holds h . x = x * u ) implies S3[h] )
assume A3: for x being Element of Q holds h . x = x * u ; :: thesis: S3[h]
S3[h]
proof
for x being Element of Q holds (f * h) . x = f . x
proof
let x be Element of Q; :: thesis: (f * h) . x = f . x
thus (f * h) . x = f . (h . x) by FUNCT_2:15
.= f . (x * u) by A3
.= (f . x) * (f . u) by Def28b
.= (f . x) * (1. Q2) by A2, Def29
.= f . x ; :: thesis: verum
end;
hence S3[h] by FUNCT_2:def 8; :: thesis: verum
end;
hence S3[h] ; :: thesis: verum
end;
A4: for u being Element of Q st u in Ker f holds
for h being Function of Q,Q st ( for x being Element of Q holds h . x = u * x ) holds
S3[h]
proof
let u be Element of Q; :: thesis: ( u in Ker f implies for h being Function of Q,Q st ( for x being Element of Q holds h . x = u * x ) holds
S3[h] )
assume A5: u in Ker f ; :: thesis: for h being Function of Q,Q st ( for x being Element of Q holds h . x = u * x ) holds
S3[h]
let h be Function of Q,Q; :: thesis: ( ( for x being Element of Q holds h . x = u * x ) implies S3[h] )
assume A6: for x being Element of Q holds h . x = u * x ; :: thesis: S3[h]
S3[h]
proof
for x being Element of Q holds (f * h) . x = f . x
proof
let x be Element of Q; :: thesis: (f * h) . x = f . x
thus (f * h) . x = f . (h . x) by FUNCT_2:15
.= f . (u * x) by A6
.= (f . u) * (f . x) by Def28b
.= (1. Q2) * (f . x) by A5, Def29
.= f . x ; :: thesis: verum
end;
hence S3[h] by FUNCT_2:def 8; :: thesis: verum
end;
hence S3[h] ; :: thesis: verum
end;
A7: for g, h being Permutation of Q st S3[g] & S3[h] holds
S3[g * h] by RELAT_1:36;
A8: for g being Permutation of Q st S3[g] holds
S3[g " ]
proof
let g be Permutation of Q; :: thesis: ( S3[g] implies S3[g " ] )
assume A9: S3[g] ; :: thesis: S3[g " ]
S3[g " ]
proof
for x being Element of Q holds (f * (g ")) . x = f . x
proof
let x be Element of Q; :: thesis: (f * (g ")) . x = f . x
thus (f * (g ")) . x = f . ((g ") . x) by FUNCT_2:15
.= f . (g . ((g ") . x)) by FUNCT_2:15, A9
.= f . ((g * (g ")) . x) by FUNCT_2:15
.= f . ((id the carrier of Q) . x) by FUNCT_2:61
.= f . x ; :: thesis: verum
end;
hence S3[g " ] by FUNCT_2:def 8; :: thesis: verum
end;
hence S3[g " ] ; :: thesis: verum
end;
for f being Function of Q,Q st f in Mlt (Ker f) holds
S3[f] from AIMLOOP:sch 1(A1, A4, A7, A8);
 hence for h being Function of Q,Q st h in Mlt (Ker f) holds
f * h = f ; :: thesis: verum