set op = the multF of F1();
set carr = the carrier of F1();
A2: dom the multF of F1() = [:the carrier of F1(),the carrier of F1():] by FUNCT_2:def 1;
A3: rng (the multF of F1() || F2()) c= F2()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (the multF of F1() || F2()) or x in F2() )
assume x in rng (the multF of F1() || F2()) ; :: thesis: x in F2()
then consider y being set such that
A4: y in dom (the multF of F1() || F2()) and
A5: x = (the multF of F1() || F2()) . y by FUNCT_1:def 5;
reconsider y = y as Element of [:F2(),F2():] by A2, A4, RELAT_1:91;
reconsider y1 = y `1 , y2 = y `2 as Element of F2() ;
y = [y1,y2] by MCART_1:23;
then x = y1 * y2 by A4, A5, FUNCT_1:70;
hence x in F2() by A1; :: thesis: verum
end;
dom (the multF of F1() || F2()) = [:F2(),F2():] by A2, RELAT_1:91;
then reconsider f = the multF of F1() || F2() as BinOp of F2() by A3, FUNCT_2:def 1, RELSET_1:11;
f c= the multF of F1() by RELAT_1:88;
then reconsider H = multMagma(# F2(),f #) as non empty strict SubStr of F1() by Def23;
take H ; :: thesis: the carrier of H = F2()
thus the carrier of H = F2() ; :: thesis: verum