let a, b, c, d be Element of F1(); :: thesis: ( P1[a,b] & P1[c,d] implies P1[F2(a,c),F2(b,d)] )
assume that
A10: P1[a,b] and
A11: P1[c,d] ; :: thesis: P1[F2(a,c),F2(b,d)]
A12: P1[F2(a,c),F2(b,c)] by A4, A10;
P1[F2(b,c),F2(c,b)] by A3;
then A13: P1[F2(a,c),F2(c,b)] by A2, A12;
P1[F2(c,b),F2(d,b)] by A4, A11;
then A14: P1[F2(a,c),F2(d,b)] by A2, A13;
P1[F2(d,b),F2(b,d)] by A3;
hence P1[F2(a,c),F2(b,d)] by A2, A14; :: thesis: verum