let L be non trivial multLoopStr_0 ; :: thesis: for z being rational_function of L holds z = [(z `1),(z `2)]
let z be rational_function of L; :: thesis: z = [(z `1),(z `2)]
consider p1 being Polynomial of L such that
H1: ex p2 being non zero Polynomial of L st z = [p1,p2] by defratf;
consider p2 being non zero Polynomial of L such that
H2: z = [p1,p2] by H1;
( z `1 = p1 & z `2 = p2 ) by H2, XTUPLE_0:def 2, XTUPLE_0:def 3;
hence z = [(z `1),(z `2)] by H2; :: thesis: verum