let H be non empty multMagma ; :: thesis: for P, Q being Subset of H holds the multF of H .: [:P,Q:] = P * Q
let P, Q be Subset of H; :: thesis: the multF of H .: [:P,Q:] = P * Q
set f = the multF of H;
A1: P * Q = { (g * h) where g, h is Element of H : ( g in P & h in Q ) } by GROUP_2:def 2;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: P * Q c= the multF of H .: [:P,Q:]

let y be set ; :: thesis: ( y in the multF of H .: [:P,Q:] implies y in P * Q )
assume y in the multF of H .: [:P,Q:] ; :: thesis: y in P * Q
then consider x being set such that
A2: ( x in [:the carrier of H,the carrier of H:] & x in [:P,Q:] & y = the multF of H . x ) by FUNCT_2:115;
consider a, b being set such that
A3: ( a in P & b in Q & x = [a,b] ) by A2, ZFMISC_1:def 2;
reconsider a = a, b = b as Element of H by A3;
y = a * b by A2, A3;
hence y in P * Q by A1, A3; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in P * Q or y in the multF of H .: [:P,Q:] )
assume y in P * Q ; :: thesis: y in the multF of H .: [:P,Q:]
then consider g, h being Element of H such that
A4: ( y = g * h & g in P & h in Q ) by A1;
( [g,h] in [:the carrier of H,the carrier of H:] & [g,h] in [:P,Q:] ) by A4, ZFMISC_1:106;
hence y in the multF of H .: [:P,Q:] by A4, FUNCT_2:43; :: thesis: verum