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;

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
x in [:the carrier of H,the carrier of H:] and
A1: x in [:P,Q:] and
A2: y = the multF of H . x by FUNCT_2:115;
consider a, b being set such that
A3: ( a in P & b in Q ) and
A4: x = [a,b] by A1, ZFMISC_1:def 2;
reconsider a = a, b = b as Element of H by A3;
y = a * b by A2, A4;
hence y in P * Q by 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
A5: y = g * h and
A6: ( g in P & h in Q ) ;
[g,h] in [:P,Q:] by A6, ZFMISC_1:106;
hence y in the multF of H .: [:P,Q:] by A5, FUNCT_2:43; :: thesis: verum