defpred S1[ set , set , set ] means ex f, g being Function st
( f = \$1 & g = \$2 & \$3 = f * g );
A1: for x, y being Element of ISOM () ex z being Element of ISOM () st S1[x,y,z]
proof
let x, y be Element of ISOM (); :: thesis: ex z being Element of ISOM () st S1[x,y,z]
reconsider x1 = x as onto isometric Function of (),() by Def4;
reconsider y1 = y as onto isometric Function of (),() by Def4;
reconsider z = x1 * y1 as Element of ISOM () by Def4;
take z ; :: thesis: S1[x,y,z]
take x1 ; :: thesis: ex g being Function st
( x1 = x & g = y & z = x1 * g )

take y1 ; :: thesis: ( x1 = x & y1 = y & z = x1 * y1 )
thus ( x1 = x & y1 = y & z = x1 * y1 ) ; :: thesis: verum
end;
consider o being BinOp of (ISOM ()) such that
A2: for a, b being Element of ISOM () holds S1[a,b,o . (a,b)] from take G = multMagma(# (ISOM ()),o #); :: thesis: ( the carrier of G = ISOM () & ( for f, g being Function st f in ISOM () & g in ISOM () holds
the multF of G . (f,g) = f * g ) )

for f, g being Function st f in ISOM () & g in ISOM () holds
the multF of G . (f,g) = f * g
proof
let f, g be Function; :: thesis: ( f in ISOM () & g in ISOM () implies the multF of G . (f,g) = f * g )
assume ( f in ISOM () & g in ISOM () ) ; :: thesis: the multF of G . (f,g) = f * g
then ex f1, g1 being Function st
( f1 = f & g1 = g & o . (f,g) = f1 * g1 ) by A2;
hence the multF of G . (f,g) = f * g ; :: thesis: verum
end;
hence ( the carrier of G = ISOM () & ( for f, g being Function st f in ISOM () & g in ISOM () holds
the multF of G . (f,g) = f * g ) ) ; :: thesis: verum