let I1, I2 be Subset of (Funcs (Q,Q)); :: thesis:
assume that
A8: for f being object holds
( f in I1 iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) and
A9: for f being object holds
( f in I2 iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) ; :: thesis:
for f being object holds
( f in I1 iff f in I2 )

let f be object ; :: thesis:
( f in I1 iff ex g being Function of Q,Q st
( f = g & g in Mlt ([#] Q) & g . (1. Q) = 1. Q ) ) by A8;
hence ( f in I1 iff f in I2 ) by A9; :: thesis:

end;